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 𝑆 ) ) )