linear_comp_law_args

forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (f : forall (x : X), Y), forall (g : forall (y : Y), Z), forall (f_linear : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f), forall (g_linear : @LinearMapLawArgs.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm g), @LinearMapLawArgs.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g)

fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun f => fun g => fun f_linear => fun g_linear => fun (P : Prop) => fun (mk : forall (map_zero_law : @Eq.{z} Z (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g xzero) zzero), forall (map_add_law : forall (x : X), forall (y : X), @Eq.{z} Z (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g (xadd x y)) (zadd (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g x) (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g y))), forall (map_neg_law : forall (x : X), @Eq.{z} Z (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g (xneg x)) (zneg (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g x))), forall (map_smul_law : forall (a : Scalar), forall (x : X), @Eq.{z} Z (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g (xsmul a x)) (zsmul a (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g x))), P) => f_linear P (fun (f_zero_arg : @Eq.{w} Y (f xzero) yzero) => fun (f_add_arg : forall (x : X), forall (y : X), @Eq.{w} Y (f (xadd x y)) (yadd (f x) (f y))) => fun (f_neg_arg : forall (x : X), @Eq.{w} Y (f (xneg x)) (yneg (f x))) => fun (f_smul_arg : forall (a : Scalar), forall (x : X), @Eq.{w} Y (f (xsmul a x)) (ysmul a (f x))) => g_linear P (fun (g_zero_arg : @Eq.{z} Z (g yzero) zzero) => fun (g_add_arg : forall (x : Y), forall (y : Y), @Eq.{z} Z (g (yadd x y)) (zadd (g x) (g y))) => fun (g_neg_arg : forall (x : Y), @Eq.{z} Z (g (yneg x)) (zneg (g x))) => fun (g_smul_arg : forall (a : Scalar), forall (x : Y), @Eq.{z} Z (g (ysmul a x)) (zsmul a (g x))) => mk (@eq_trans.{z} Z (g (f xzero)) (g yzero) zzero (@eq_congr_arg.{w,z} Y Z g (f xzero) yzero f_zero_arg) g_zero_arg) (fun (x : X) => fun (y : X) => @eq_trans.{z} Z (g (f (xadd x y))) (g (yadd (f x) (f y))) (zadd (g (f x)) (g (f y))) (@eq_congr_arg.{w,z} Y Z g (f (xadd x y)) (yadd (f x) (f y)) (f_add_arg x y)) (g_add_arg (f x) (f y))) (fun (x : X) => @eq_trans.{z} Z (g (f (xneg x))) (g (yneg (f x))) (zneg (g (f x))) (@eq_congr_arg.{w,z} Y Z g (f (xneg x)) (yneg (f x)) (f_neg_arg x)) (g_neg_arg (f x))) (fun (a : Scalar) => fun (x : X) => @eq_trans.{z} Z (g (f (xsmul a x))) (g (ysmul a (f x))) (zsmul a (g (f x))) (@eq_congr_arg.{w,z} Y Z g (f (xsmul a x)) (ysmul a (f x)) (f_smul_arg a x)) (g_smul_arg a (f x)))))