Metamath Proof Explorer

Theorem lmhmf1o

Description: A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Hypotheses lmhmf1o.x 
|- X = ( Base ` S )
lmhmf1o.y 
|- Y = ( Base ` T )
Assertion lmhmf1o 
|- ( F e. ( S LMHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T LMHom S ) ) )

Proof

Step Hyp Ref Expression
1 lmhmf1o.x 
 |-  X = ( Base ` S )
2 lmhmf1o.y 
 |-  Y = ( Base ` T )
3 eqid 
 |-  ( .s ` T ) = ( .s ` T )
4 eqid 
 |-  ( .s ` S ) = ( .s ` S )
5 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
6 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
7 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
8 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
9 8 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> T e. LMod )
10 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
11 10 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> S e. LMod )
12 6 5 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = ( Scalar ` S ) )
13 12 eqcomd 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` S ) = ( Scalar ` T ) )
14 13 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> ( Scalar ` S ) = ( Scalar ` T ) )
15 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
16 1 2 ghmf1o 
 |-  ( F e. ( S GrpHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) )
17 15 16 syl 
 |-  ( F e. ( S LMHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) )
18 17 biimpa 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> `' F e. ( T GrpHom S ) )
19 simpll 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> F e. ( S LMHom T ) )
20 14 fveq2d 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` T ) ) )
21 20 eleq2d 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> ( a e. ( Base ` ( Scalar ` S ) ) <-> a e. ( Base ` ( Scalar ` T ) ) ) )
22 21 biimpar 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ a e. ( Base ` ( Scalar ` T ) ) ) -> a e. ( Base ` ( Scalar ` S ) ) )
23 22 adantrr 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> a e. ( Base ` ( Scalar ` S ) ) )
24 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
25 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
26 24 25 syl 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y --> X )
27 26 adantl 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> `' F : Y --> X )
28 27 ffvelcdmda 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ b e. Y ) -> ( `' F ` b ) e. X )
29 28 adantrl 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( `' F ` b ) e. X )
30 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
31 6 30 1 4 3 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ a e. ( Base ` ( Scalar ` S ) ) /\ ( `' F ` b ) e. X ) -> ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) ( F ` ( `' F ` b ) ) ) )
32 19 23 29 31 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) ( F ` ( `' F ` b ) ) ) )
33 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ b e. Y ) -> ( F ` ( `' F ` b ) ) = b )
34 33 ad2ant2l 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( F ` ( `' F ` b ) ) = b )
35 34 oveq2d 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( a ( .s ` T ) ( F ` ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) )
36 32 35 eqtrd 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) )
37 simplr 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> F : X -1-1-onto-> Y )
38 11 adantr 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> S e. LMod )
39 1 6 4 30 lmodvscl 
 |-  ( ( S e. LMod /\ a e. ( Base ` ( Scalar ` S ) ) /\ ( `' F ` b ) e. X ) -> ( a ( .s ` S ) ( `' F ` b ) ) e. X )
40 38 23 29 39 syl3anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( a ( .s ` S ) ( `' F ` b ) ) e. X )
41 f1ocnvfv 
 |-  ( ( F : X -1-1-onto-> Y /\ ( a ( .s ` S ) ( `' F ` b ) ) e. X ) -> ( ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) -> ( `' F ` ( a ( .s ` T ) b ) ) = ( a ( .s ` S ) ( `' F ` b ) ) ) )
42 37 40 41 syl2anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) -> ( `' F ` ( a ( .s ` T ) b ) ) = ( a ( .s ` S ) ( `' F ` b ) ) ) )
43 36 42 mpd 
 |-  ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( `' F ` ( a ( .s ` T ) b ) ) = ( a ( .s ` S ) ( `' F ` b ) ) )
44 2 3 4 5 6 7 9 11 14 18 43 islmhmd 
 |-  ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> `' F e. ( T LMHom S ) )
45 1 2 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : X --> Y )
46 45 ffnd 
 |-  ( F e. ( S LMHom T ) -> F Fn X )
47 46 adantr 
 |-  ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> F Fn X )
48 2 1 lmhmf 
 |-  ( `' F e. ( T LMHom S ) -> `' F : Y --> X )
49 48 adantl 
 |-  ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> `' F : Y --> X )
50 49 ffnd 
 |-  ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> `' F Fn Y )
51 dff1o4 
 |-  ( F : X -1-1-onto-> Y <-> ( F Fn X /\ `' F Fn Y ) )
52 47 50 51 sylanbrc 
 |-  ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> F : X -1-1-onto-> Y )
53 44 52 impbida 
 |-  ( F e. ( S LMHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T LMHom S ) ) )