Metamath Proof Explorer

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	$⊢ (F \in (S LMIso T) \land G \in (R LMIso S)) \to F \circ G \in (R LMIso T)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{S} = {Base}_{S}$
2		eqid	$⊢ {Base}_{T} = {Base}_{T}$
3	1 2	islmim	$⊢ F \in (S LMIso T) \leftrightarrow (F \in (S LMHom T) \land F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T})$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4 1	islmim	$⊢ G \in (R LMIso S) \leftrightarrow (G \in (R LMHom S) \land G : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
6		lmhmco	$⊢ (F \in (S LMHom T) \land G \in (R LMHom S)) \to F \circ G \in (R LMHom T)$
7	6	ad2ant2r	$⊢ ((F \in (S LMHom T) \land F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T}) \land (G \in (R LMHom S) \land G : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})) \to F \circ G \in (R LMHom T)$
8		f1oco	$⊢ (F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T} \land G : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}) \to (F \circ G) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{T}$
9	8	ad2ant2l	$⊢ ((F \in (S LMHom T) \land F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T}) \land (G \in (R LMHom S) \land G : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})) \to (F \circ G) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{T}$
10	4 2	islmim	$⊢ F \circ G \in (R LMIso T) \leftrightarrow (F \circ G \in (R LMHom T) \land (F \circ G) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{T})$
11	7 9 10	sylanbrc	$⊢ ((F \in (S LMHom T) \land F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T}) \land (G \in (R LMHom S) \land G : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})) \to F \circ G \in (R LMIso T)$
12	3 5 11	syl2anb	$⊢ (F \in (S LMIso T) \land G \in (R LMIso S)) \to F \circ G \in (R LMIso T)$