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 𝑋 = ( Base ‘ 𝑆 )
lmhmf1o.y 𝑌 = ( Base ‘ 𝑇 )
Assertion lmhmf1o ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 lmhmf1o.x 𝑋 = ( Base ‘ 𝑆 )
2 lmhmf1o.y 𝑌 = ( Base ‘ 𝑇 )
3 eqid ( ·𝑠𝑇 ) = ( ·𝑠𝑇 )
4 eqid ( ·𝑠𝑆 ) = ( ·𝑠𝑆 )
5 eqid ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
6 eqid ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
7 eqid ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
8 lmhmlmod2 ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
9 8 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → 𝑇 ∈ LMod )
10 lmhmlmod1 ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
11 10 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → 𝑆 ∈ LMod )
12 6 5 lmhmsca ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
13 12 eqcomd ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑇 ) )
14 13 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑇 ) )
15 lmghm ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
16 1 2 ghmf1o ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) )
17 15 16 syl ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) )
18 17 biimpa ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) )
19 simpll ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
20 14 fveq2d ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
21 20 eleq2d ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) )
22 21 biimpar ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
23 22 adantrr ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
24 f1ocnv ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 : 𝑌1-1-onto𝑋 )
25 f1of ( 𝐹 : 𝑌1-1-onto𝑋 𝐹 : 𝑌𝑋 )
26 24 25 syl ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 : 𝑌𝑋 )
27 26 adantl ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → 𝐹 : 𝑌𝑋 )
28 27 ffvelrnda ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ 𝑏𝑌 ) → ( 𝐹𝑏 ) ∈ 𝑋 )
29 28 adantrl ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝐹𝑏 ) ∈ 𝑋 )
30 eqid ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
31 6 30 1 4 3 lmhmlin ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ ( 𝐹𝑏 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) = ( 𝑎 ( ·𝑠𝑇 ) ( 𝐹 ‘ ( 𝐹𝑏 ) ) ) )
32 19 23 29 31 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) = ( 𝑎 ( ·𝑠𝑇 ) ( 𝐹 ‘ ( 𝐹𝑏 ) ) ) )
33 f1ocnvfv2 ( ( 𝐹 : 𝑋1-1-onto𝑌𝑏𝑌 ) → ( 𝐹 ‘ ( 𝐹𝑏 ) ) = 𝑏 )
34 33 ad2ant2l ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝐹 ‘ ( 𝐹𝑏 ) ) = 𝑏 )
35 34 oveq2d ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝑎 ( ·𝑠𝑇 ) ( 𝐹 ‘ ( 𝐹𝑏 ) ) ) = ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) )
36 32 35 eqtrd ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) = ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) )
37 simplr ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → 𝐹 : 𝑋1-1-onto𝑌 )
38 11 adantr ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → 𝑆 ∈ LMod )
39 1 6 4 30 lmodvscl ( ( 𝑆 ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ ( 𝐹𝑏 ) ∈ 𝑋 ) → ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ∈ 𝑋 )
40 38 23 29 39 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ∈ 𝑋 )
41 f1ocnvfv ( ( 𝐹 : 𝑋1-1-onto𝑌 ∧ ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) = ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) )
42 37 40 41 syl2anc ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) = ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) ) )
43 36 42 mpd ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏𝑌 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠𝑇 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠𝑆 ) ( 𝐹𝑏 ) ) )
44 2 3 4 5 6 7 9 11 14 18 43 islmhmd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋1-1-onto𝑌 ) → 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) )
45 1 2 lmhmf ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑋𝑌 )
46 45 ffnd ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 Fn 𝑋 )
47 46 adantr ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → 𝐹 Fn 𝑋 )
48 2 1 lmhmf ( 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) → 𝐹 : 𝑌𝑋 )
49 48 adantl ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → 𝐹 : 𝑌𝑋 )
50 49 ffnd ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → 𝐹 Fn 𝑌 )
51 dff1o4 ( 𝐹 : 𝑋1-1-onto𝑌 ↔ ( 𝐹 Fn 𝑋 𝐹 Fn 𝑌 ) )
52 47 50 51 sylanbrc ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → 𝐹 : 𝑋1-1-onto𝑌 )
53 44 52 impbida ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 : 𝑋1-1-onto𝑌 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) )