lmictra

Description: Module isomorphism is transitive. (Contributed by AV, 10-Mar-2019)

		Ref	Expression
	Assertion	lmictra	$⊢ (R ≃_{𝑚} S \land S ≃_{𝑚} T) \to R ≃_{𝑚} T$

Step	Hyp	Ref	Expression
1		brlmic	$⊢ R ≃_{𝑚} S \leftrightarrow R LMIso S \neq \emptyset$
2		brlmic	$⊢ S ≃_{𝑚} T \leftrightarrow S LMIso T \neq \emptyset$
3		n0	$⊢ R LMIso S \neq \emptyset \leftrightarrow \exists g g \in (R LMIso S)$
4		n0	$⊢ S LMIso T \neq \emptyset \leftrightarrow \exists f f \in (S LMIso T)$
5		lmimco	$⊢ (f \in (S LMIso T) \land g \in (R LMIso S)) \to f \circ g \in (R LMIso T)$
6		brlmici	$⊢ f \circ g \in (R LMIso T) \to R ≃_{𝑚} T$
7	5 6	syl	$⊢ (f \in (S LMIso T) \land g \in (R LMIso S)) \to R ≃_{𝑚} T$
8	7	ex	$⊢ f \in (S LMIso T) \to (g \in (R LMIso S) \to R ≃_{𝑚} T)$
9	8	exlimiv	$⊢ \exists f f \in (S LMIso T) \to (g \in (R LMIso S) \to R ≃_{𝑚} T)$
10	9	com12	$⊢ g \in (R LMIso S) \to (\exists f f \in (S LMIso T) \to R ≃_{𝑚} T)$
11	10	exlimiv	$⊢ \exists g g \in (R LMIso S) \to (\exists f f \in (S LMIso T) \to R ≃_{𝑚} T)$
12	11	imp	$⊢ (\exists g g \in (R LMIso S) \land \exists f f \in (S LMIso T)) \to R ≃_{𝑚} T$
13	3 4 12	syl2anb	$⊢ (R LMIso S \neq \emptyset \land S LMIso T \neq \emptyset) \to R ≃_{𝑚} T$
14	1 2 13	syl2anb	$⊢ (R ≃_{𝑚} S \land S ≃_{𝑚} T) \to R ≃_{𝑚} T$

Metamath Proof Explorer