This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lmim

Description: An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Assertion df-lmim LMIso = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmim ⊢ LMIso
1 vs ⊢ 𝑠
2 clmod ⊢ LMod
3 vt ⊢ 𝑡
4 vg ⊢ 𝑔
5 1 cv ⊢ 𝑠
6 clmhm ⊢ LMHom
7 3 cv ⊢ 𝑡
8 5 7 6 co ⊢ ( 𝑠 LMHom 𝑡 )
9 4 cv ⊢ 𝑔
10 cbs ⊢ Base
11 5 10 cfv ⊢ ( Base ‘ 𝑠 )
12 7 10 cfv ⊢ ( Base ‘ 𝑡 )
13 11 12 9 wf1o ⊢ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 )
14 13 4 8 crab ⊢ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) }
15 1 3 2 2 14 cmpo ⊢ ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )
16 0 15 wceq ⊢ LMIso = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )