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 ffvelrnda
 |-  ( ( ( 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 ) ) )