Metamath Proof Explorer

Theorem islmhm

Description: Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015) (Proof shortened by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses islmhm.k 
|- K = ( Scalar ` S )
islmhm.l 
|- L = ( Scalar ` T )
islmhm.b 
|- B = ( Base ` K )
islmhm.e 
|- E = ( Base ` S )
islmhm.m 
|- .x. = ( .s ` S )
islmhm.n 
|- .X. = ( .s ` T )
Assertion islmhm 
|- ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islmhm.k 
 |-  K = ( Scalar ` S )
2 islmhm.l 
 |-  L = ( Scalar ` T )
3 islmhm.b 
 |-  B = ( Base ` K )
4 islmhm.e 
 |-  E = ( Base ` S )
5 islmhm.m 
 |-  .x. = ( .s ` S )
6 islmhm.n 
 |-  .X. = ( .s ` T )
7 df-lmhm 
 |-  LMHom = ( s e. LMod , t e. LMod |-> { f e. ( s GrpHom t ) | [. ( Scalar ` s ) / w ]. ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } )
8 7 elmpocl 
 |-  ( F e. ( S LMHom T ) -> ( S e. LMod /\ T e. LMod ) )
9 oveq12 
 |-  ( ( s = S /\ t = T ) -> ( s GrpHom t ) = ( S GrpHom T ) )
10 fvexd 
 |-  ( ( s = S /\ t = T ) -> ( Scalar ` s ) e. _V )
11 simplr 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> t = T )
12 11 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Scalar ` t ) = ( Scalar ` T ) )
13 12 2 eqtr4di 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Scalar ` t ) = L )
14 simpr 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> w = ( Scalar ` s ) )
15 simpll 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> s = S )
16 15 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Scalar ` s ) = ( Scalar ` S ) )
17 14 16 eqtrd 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> w = ( Scalar ` S ) )
18 17 1 eqtr4di 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> w = K )
19 13 18 eqeq12d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( ( Scalar ` t ) = w <-> L = K ) )
20 18 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Base ` w ) = ( Base ` K ) )
21 20 3 eqtr4di 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Base ` w ) = B )
22 15 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Base ` s ) = ( Base ` S ) )
23 22 4 eqtr4di 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( Base ` s ) = E )
24 15 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( .s ` s ) = ( .s ` S ) )
25 24 5 eqtr4di 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( .s ` s ) = .x. )
26 25 oveqd 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( x ( .s ` s ) y ) = ( x .x. y ) )
27 26 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( f ` ( x ( .s ` s ) y ) ) = ( f ` ( x .x. y ) ) )
28 11 fveq2d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( .s ` t ) = ( .s ` T ) )
29 28 6 eqtr4di 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( .s ` t ) = .X. )
30 29 oveqd 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( x ( .s ` t ) ( f ` y ) ) = ( x .X. ( f ` y ) ) )
31 27 30 eqeq12d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) <-> ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) )
32 23 31 raleqbidv 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) <-> A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) )
33 21 32 raleqbidv 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) <-> A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) )
34 19 33 anbi12d 
 |-  ( ( ( s = S /\ t = T ) /\ w = ( Scalar ` s ) ) -> ( ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) <-> ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) ) )
35 10 34 sbcied 
 |-  ( ( s = S /\ t = T ) -> ( [. ( Scalar ` s ) / w ]. ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) <-> ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) ) )
36 9 35 rabeqbidv 
 |-  ( ( s = S /\ t = T ) -> { f e. ( s GrpHom t ) | [. ( Scalar ` s ) / w ]. ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } = { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } )
37 ovex 
 |-  ( S GrpHom T ) e. _V
38 37 rabex 
 |-  { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } e. _V
39 36 7 38 ovmpoa 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( S LMHom T ) = { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } )
40 39 eleq2d 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> F e. { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } ) )
41 fveq1 
 |-  ( f = F -> ( f ` ( x .x. y ) ) = ( F ` ( x .x. y ) ) )
42 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
43 42 oveq2d 
 |-  ( f = F -> ( x .X. ( f ` y ) ) = ( x .X. ( F ` y ) ) )
44 41 43 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) <-> ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
45 44 2ralbidv 
 |-  ( f = F -> ( A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) <-> A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
46 45 anbi2d 
 |-  ( f = F -> ( ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) <-> ( L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
47 46 elrab 
 |-  ( F e. { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } <-> ( F e. ( S GrpHom T ) /\ ( L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
48 3anass 
 |-  ( ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) <-> ( F e. ( S GrpHom T ) /\ ( L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
49 47 48 bitr4i 
 |-  ( F e. { f e. ( S GrpHom T ) | ( L = K /\ A. x e. B A. y e. E ( f ` ( x .x. y ) ) = ( x .X. ( f ` y ) ) ) } <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) )
50 40 49 bitrdi 
 |-  ( ( S e. LMod /\ T e. LMod ) -> ( F e. ( S LMHom T ) <-> ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )
51 8 50 biadanii 
 |-  ( F e. ( S LMHom T ) <-> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K /\ A. x e. B A. y e. E ( F ` ( x .x. y ) ) = ( x .X. ( F ` y ) ) ) ) )