Metamath Proof Explorer

Theorem islmim

Description: An isomorphism of left modules is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Hypotheses islmim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
islmim.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
Assertion islmim ( 𝐹 ∈ ( 𝑅 LMIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 islmim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 islmim.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 df-lmim ⊢ LMIso = ( 𝑎 ∈ LMod , 𝑏 ∈ LMod ↦ { 𝑐 ∈ ( 𝑎 LMHom 𝑏 ) ∣ 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) } )
4 ovex ⊢ ( 𝑎 LMHom 𝑏 ) ∈ V
5 4 rabex ⊢ { 𝑐 ∈ ( 𝑎 LMHom 𝑏 ) ∣ 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) } ∈ V
6 oveq12 ⊢ ( ( 𝑎 = 𝑅 ∧ 𝑏 = 𝑆 ) → ( 𝑎 LMHom 𝑏 ) = ( 𝑅 LMHom 𝑆 ) )
7 fveq2 ⊢ ( 𝑎 = 𝑅 → ( Base ‘ 𝑎 ) = ( Base ‘ 𝑅 ) )
8 7 1 eqtr4di ⊢ ( 𝑎 = 𝑅 → ( Base ‘ 𝑎 ) = 𝐵 )
9 fveq2 ⊢ ( 𝑏 = 𝑆 → ( Base ‘ 𝑏 ) = ( Base ‘ 𝑆 ) )
10 9 2 eqtr4di ⊢ ( 𝑏 = 𝑆 → ( Base ‘ 𝑏 ) = 𝐶 )
11 f1oeq23 ⊢ ( ( ( Base ‘ 𝑎 ) = 𝐵 ∧ ( Base ‘ 𝑏 ) = 𝐶 ) → ( 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) ↔ 𝑐 : 𝐵 –1-1-onto→ 𝐶 ) )
12 8 10 11 syl2an ⊢ ( ( 𝑎 = 𝑅 ∧ 𝑏 = 𝑆 ) → ( 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) ↔ 𝑐 : 𝐵 –1-1-onto→ 𝐶 ) )
13 6 12 rabeqbidv ⊢ ( ( 𝑎 = 𝑅 ∧ 𝑏 = 𝑆 ) → { 𝑐 ∈ ( 𝑎 LMHom 𝑏 ) ∣ 𝑐 : ( Base ‘ 𝑎 ) –1-1-onto→ ( Base ‘ 𝑏 ) } = { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } )
14 3 5 13 elovmpo ⊢ ( 𝐹 ∈ ( 𝑅 LMIso 𝑆 ) ↔ ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) )
15 df-3an ⊢ ( ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) ↔ ( ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) )
16 f1oeq1 ⊢ ( 𝑐 = 𝐹 → ( 𝑐 : 𝐵 –1-1-onto→ 𝐶 ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
17 16 elrab ⊢ ( 𝐹 ∈ { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ↔ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
18 17 anbi2i ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) ↔ ( ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) )
19 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) → 𝑅 ∈ LMod )
20 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) → 𝑆 ∈ LMod )
21 19 20 jca ⊢ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) → ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) )
22 21 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) )
23 22 pm4.71ri ⊢ ( ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ↔ ( ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) )
24 18 23 bitr4i ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝑆 ∈ LMod ) ∧ 𝐹 ∈ { 𝑐 ∈ ( 𝑅 LMHom 𝑆 ) ∣ 𝑐 : 𝐵 –1-1-onto→ 𝐶 } ) ↔ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )
25 14 15 24 3bitri ⊢ ( 𝐹 ∈ ( 𝑅 LMIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) )