This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islmhm2

Description: A one-equation proof of linearity of a left module homomorphism, similar to df-lss . (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses islmhm2.b 
|- B = ( Base ` S )
islmhm2.c 
|- C = ( Base ` T )
islmhm2.k 
|- K = ( Scalar ` S )
islmhm2.l 
|- L = ( Scalar ` T )
islmhm2.e 
|- E = ( Base ` K )
islmhm2.p 
|- .+ = ( +g ` S )
islmhm2.q 
|- .+^ = ( +g ` T )
islmhm2.m 
|- .x. = ( .s ` S )
islmhm2.n 
|- .X. = ( .s ` T )
Assertion islmhm2 
|- ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islmhm2.b 
 |-  B = ( Base ` S )
2 islmhm2.c 
 |-  C = ( Base ` T )
3 islmhm2.k 
 |-  K = ( Scalar ` S )
4 islmhm2.l 
 |-  L = ( Scalar ` T )
5 islmhm2.e 
 |-  E = ( Base ` K )
6 islmhm2.p 
 |-  .+ = ( +g ` S )
7 islmhm2.q 
 |-  .+^ = ( +g ` T )
8 islmhm2.m 
 |-  .x. = ( .s ` S )
9 islmhm2.n 
 |-  .X. = ( .s ` T )
10 1 2 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : B --> C )
11 3 4 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> L = K )
12 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
13 12 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> F e. ( S GrpHom T ) )
14 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
15 14 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> S e. LMod )
16 simpr1 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> x e. E )
17 simpr2 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> y e. B )
18 1 3 8 5 lmodvscl 
 |-  ( ( S e. LMod /\ x e. E /\ y e. B ) -> ( x .x. y ) e. B )
19 15 16 17 18 syl3anc 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> ( x .x. y ) e. B )
20 simpr3 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> z e. B )
21 1 6 7 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ ( x .x. y ) e. B /\ z e. B ) -> ( F ` ( ( x .x. y ) .+ z ) ) = ( ( F ` ( x .x. y ) ) .+^ ( F ` z ) ) )
22 13 19 20 21 syl3anc 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> ( F ` ( ( x .x. y ) .+ z ) ) = ( ( F ` ( x .x. y ) ) .+^ ( F ` z ) ) )
23 3 5 1 8 9 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ x e. E /\ y e. B ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
24 23 3adant3r3 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
25 24 oveq1d 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> ( ( F ` ( x .x. y ) ) .+^ ( F ` z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) )
26 22 25 eqtrd 
 |-  ( ( F e. ( S LMHom T ) /\ ( x e. E /\ y e. B /\ z e. B ) ) -> ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) )
27 26 ralrimivvva 
 |-  ( F e. ( S LMHom T ) -> A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) )
28 10 11 27 3jca 
 |-  ( F e. ( S LMHom T ) -> ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) )
29 28 adantl 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ F e. ( S LMHom T ) ) -> ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) )
30 lmodgrp 
 |-  ( S e. LMod -> S e. Grp )
31 lmodgrp 
 |-  ( T e. LMod -> T e. Grp )
32 30 31 anim12i 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( S e. Grp /\ T e. Grp ) )
33 32 adantr 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> ( S e. Grp /\ T e. Grp ) )
34 simpr1 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> F : B --> C )
35 3 lmodring 
 |-  ( S e. LMod -> K e. Ring )
36 35 ad2antrr 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) -> K e. Ring )
37 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
38 5 37 ringidcl 
 |-  ( K e. Ring -> ( 1r ` K ) e. E )
39 oveq1 
 |-  ( x = ( 1r ` K ) -> ( x .x. y ) = ( ( 1r ` K ) .x. y ) )
40 39 fvoveq1d 
 |-  ( x = ( 1r ` K ) -> ( F ` ( ( x .x. y ) .+ z ) ) = ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) )
41 oveq1 
 |-  ( x = ( 1r ` K ) -> ( x .X. ( F ` y ) ) = ( ( 1r ` K ) .X. ( F ` y ) ) )
42 41 oveq1d 
 |-  ( x = ( 1r ` K ) -> ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) )
43 40 42 eqeq12d 
 |-  ( x = ( 1r ` K ) -> ( ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) <-> ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) ) )
44 43 2ralbidv 
 |-  ( x = ( 1r ` K ) -> ( A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) <-> A. y e. B A. z e. B ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) ) )
45 44 rspcv 
 |-  ( ( 1r ` K ) e. E -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> A. y e. B A. z e. B ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) ) )
46 36 38 45 3syl 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> A. y e. B A. z e. B ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) ) )
47 simplll 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> S e. LMod )
48 simprl 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> y e. B )
49 1 3 8 37 lmodvs1 
 |-  ( ( S e. LMod /\ y e. B ) -> ( ( 1r ` K ) .x. y ) = y )
50 47 48 49 syl2anc 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( 1r ` K ) .x. y ) = y )
51 50 fvoveq1d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( F ` ( y .+ z ) ) )
52 simplrr 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> L = K )
53 52 fveq2d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( 1r ` L ) = ( 1r ` K ) )
54 53 oveq1d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( 1r ` L ) .X. ( F ` y ) ) = ( ( 1r ` K ) .X. ( F ` y ) ) )
55 simpllr 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> T e. LMod )
56 simplrl 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> F : B --> C )
57 56 48 ffvelcdmd 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( F ` y ) e. C )
58 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
59 2 4 9 58 lmodvs1 
 |-  ( ( T e. LMod /\ ( F ` y ) e. C ) -> ( ( 1r ` L ) .X. ( F ` y ) ) = ( F ` y ) )
60 55 57 59 syl2anc 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( 1r ` L ) .X. ( F ` y ) ) = ( F ` y ) )
61 54 60 eqtr3d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( 1r ` K ) .X. ( F ` y ) ) = ( F ` y ) )
62 61 oveq1d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) )
63 51 62 eqeq12d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) <-> ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) ) )
64 63 2ralbidva 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) -> ( A. y e. B A. z e. B ( F ` ( ( ( 1r ` K ) .x. y ) .+ z ) ) = ( ( ( 1r ` K ) .X. ( F ` y ) ) .+^ ( F ` z ) ) <-> A. y e. B A. z e. B ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) ) )
65 46 64 sylibd 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K ) ) -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> A. y e. B A. z e. B ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) ) )
66 65 exp32 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F : B --> C -> ( L = K -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> A. y e. B A. z e. B ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) ) ) ) )
67 66 3imp2 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> A. y e. B A. z e. B ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) )
68 34 67 jca 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> ( F : B --> C /\ A. y e. B A. z e. B ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) ) )
69 1 2 6 7 isghm 
 |-  ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : B --> C /\ A. y e. B A. z e. B ( F ` ( y .+ z ) ) = ( ( F ` y ) .+^ ( F ` z ) ) ) ) )
70 33 68 69 sylanbrc 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> F e. ( S GrpHom T ) )
71 simpr2 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> L = K )
72 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
73 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
74 72 73 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
75 70 74 syl 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
76 30 ad3antrrr 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> S e. Grp )
77 1 72 grpidcl 
 |-  ( S e. Grp -> ( 0g ` S ) e. B )
78 oveq2 
 |-  ( z = ( 0g ` S ) -> ( ( x .x. y ) .+ z ) = ( ( x .x. y ) .+ ( 0g ` S ) ) )
79 78 fveq2d 
 |-  ( z = ( 0g ` S ) -> ( F ` ( ( x .x. y ) .+ z ) ) = ( F ` ( ( x .x. y ) .+ ( 0g ` S ) ) ) )
80 fveq2 
 |-  ( z = ( 0g ` S ) -> ( F ` z ) = ( F ` ( 0g ` S ) ) )
81 80 oveq2d 
 |-  ( z = ( 0g ` S ) -> ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) )
82 79 81 eqeq12d 
 |-  ( z = ( 0g ` S ) -> ( ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) <-> ( F ` ( ( x .x. y ) .+ ( 0g ` S ) ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) ) )
83 82 rspcv 
 |-  ( ( 0g ` S ) e. B -> ( A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> ( F ` ( ( x .x. y ) .+ ( 0g ` S ) ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) ) )
84 76 77 83 3syl 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> ( F ` ( ( x .x. y ) .+ ( 0g ` S ) ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) ) )
85 simplll 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> S e. LMod )
86 simprl 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> x e. E )
87 simprr 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> y e. B )
88 85 86 87 18 syl3anc 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( x .x. y ) e. B )
89 1 6 72 grprid 
 |-  ( ( S e. Grp /\ ( x .x. y ) e. B ) -> ( ( x .x. y ) .+ ( 0g ` S ) ) = ( x .x. y ) )
90 76 88 89 syl2anc 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( ( x .x. y ) .+ ( 0g ` S ) ) = ( x .x. y ) )
91 90 fveq2d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( F ` ( ( x .x. y ) .+ ( 0g ` S ) ) ) = ( F ` ( x .x. y ) ) )
92 simplr3 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
93 92 oveq2d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) = ( ( x .X. ( F ` y ) ) .+^ ( 0g ` T ) ) )
94 simpllr 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> T e. LMod )
95 94 31 syl 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> T e. Grp )
96 simplr2 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> L = K )
97 96 fveq2d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( Base ` L ) = ( Base ` K ) )
98 97 5 eqtr4di 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( Base ` L ) = E )
99 86 98 eleqtrrd 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> x e. ( Base ` L ) )
100 simplr1 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> F : B --> C )
101 100 87 ffvelcdmd 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( F ` y ) e. C )
102 eqid 
 |-  ( Base ` L ) = ( Base ` L )
103 2 4 9 102 lmodvscl 
 |-  ( ( T e. LMod /\ x e. ( Base ` L ) /\ ( F ` y ) e. C ) -> ( x .X. ( F ` y ) ) e. C )
104 94 99 101 103 syl3anc 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( x .X. ( F ` y ) ) e. C )
105 2 7 73 grprid 
 |-  ( ( T e. Grp /\ ( x .X. ( F ` y ) ) e. C ) -> ( ( x .X. ( F ` y ) ) .+^ ( 0g ` T ) ) = ( x .X. ( F ` y ) ) )
106 95 104 105 syl2anc 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( ( x .X. ( F ` y ) ) .+^ ( 0g ` T ) ) = ( x .X. ( F ` y ) ) )
107 93 106 eqtrd 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) = ( x .X. ( F ` y ) ) )
108 91 107 eqeq12d 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( ( F ` ( ( x .x. y ) .+ ( 0g ` S ) ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` ( 0g ` S ) ) ) <-> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
109 84 108 sylibd 
 |-  ( ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) /\ ( x e. E /\ y e. B ) ) -> ( A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
110 109 ralimdvva 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
111 110 3exp2 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F : B --> C -> ( L = K -> ( ( F ` ( 0g ` S ) ) = ( 0g ` T ) -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) ) ) )
112 111 com45 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F : B --> C -> ( L = K -> ( A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) -> ( ( F ` ( 0g ` S ) ) = ( 0g ` T ) -> A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) ) ) )
113 112 3imp2 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> ( ( F ` ( 0g ` S ) ) = ( 0g ` T ) -> A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
114 75 113 mpd 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) )
115 3 4 5 1 8 9 islmhm3 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
116 115 adantr 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. E A. y e. B ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
117 70 71 114 116 mpbir3and 
 |-  ( ( ( S e. LMod /\ T e. LMod ) /\ ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) -> F e. ( S LMHom T ) )
118 29 117 impbida 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F : B --> C /\ L = K /\ A. x e. E A. y e. B A. z e. B ( F ` ( ( x .x. y ) .+ z ) ) = ( ( x .X. ( F ` y ) ) .+^ ( F ` z ) ) ) ) )