Theorem lmimco

Description: The composition of two isomorphisms of modules is an isomorphism of modules. (Contributed by AV, 10-Mar-2019)

	Ref	Expression
Assertion	lmimco	⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 LMIso 𝑆 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMIso 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
2		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
3	1 2	islmim	⊢ ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) ) )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	4 1	islmim	⊢ ( 𝐺 ∈ ( 𝑅 LMIso 𝑆 ) ↔ ( 𝐺 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐺 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) )
6		lmhmco	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 LMHom 𝑆 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMHom 𝑇 ) )
7	6	ad2ant2r	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) ) ∧ ( 𝐺 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐺 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMHom 𝑇 ) )
8		f1oco	⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) ∧ 𝐺 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) → ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
9	8	ad2ant2l	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) ) ∧ ( 𝐺 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐺 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
10	4 2	islmim	⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMIso 𝑇 ) ↔ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMHom 𝑇 ) ∧ ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑇 ) ) )
11	7 9 10	sylanbrc	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) ) ∧ ( 𝐺 ∈ ( 𝑅 LMHom 𝑆 ) ∧ 𝐺 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMIso 𝑇 ) )
12	3 5 11	syl2anb	⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 LMIso 𝑆 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 LMIso 𝑇 ) )