rngoisoco

Description: The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

		Ref	Expression
	Assertion	rngoisoco	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to G \circ F \in (R RingOpsIso T)$

Proof

Step	Hyp	Ref	Expression
1		rngoisohom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to F \in (R RingOpsHom S)$
2	1	3expa	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsIso S)) \to F \in (R RingOpsHom S)$
3	2	3adantl3	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land F \in (R RingOpsIso S)) \to F \in (R RingOpsHom S)$
4		rngoisohom	$⊢ (S \in RingOps \land T \in RingOps \land G \in (S RingOpsIso T)) \to G \in (S RingOpsHom T)$
5	4	3expa	$⊢ ((S \in RingOps \land T \in RingOps) \land G \in (S RingOpsIso T)) \to G \in (S RingOpsHom T)$
6	5	3adantl1	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land G \in (S RingOpsIso T)) \to G \in (S RingOpsHom T)$
7	3 6	anim12dan	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to (F \in (R RingOpsHom S) \land G \in (S RingOpsHom T))$
8		rngohomco	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsHom S) \land G \in (S RingOpsHom T))) \to G \circ F \in (R RingOpsHom T)$
9	7 8	syldan	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to G \circ F \in (R RingOpsHom T)$
10		eqid	$⊢ 1^{st} (S) = 1^{st} (S)$
11		eqid	$⊢ ran 1^{st} (S) = ran 1^{st} (S)$
12		eqid	$⊢ 1^{st} (T) = 1^{st} (T)$
13		eqid	$⊢ ran 1^{st} (T) = ran 1^{st} (T)$
14	10 11 12 13	rngoiso1o	$⊢ (S \in RingOps \land T \in RingOps \land G \in (S RingOpsIso T)) \to G : ran 1^{st} (S) \underset{1-1 onto}{⟶} ran 1^{st} (T)$
15	14	3expa	$⊢ ((S \in RingOps \land T \in RingOps) \land G \in (S RingOpsIso T)) \to G : ran 1^{st} (S) \underset{1-1 onto}{⟶} ran 1^{st} (T)$
16	15	3adantl1	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land G \in (S RingOpsIso T)) \to G : ran 1^{st} (S) \underset{1-1 onto}{⟶} ran 1^{st} (T)$
17	16	adantrl	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to G : ran 1^{st} (S) \underset{1-1 onto}{⟶} ran 1^{st} (T)$
18		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
19		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
20	18 19 10 11	rngoiso1o	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to F : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (S)$
21	20	3expa	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsIso S)) \to F : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (S)$
22	21	3adantl3	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land F \in (R RingOpsIso S)) \to F : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (S)$
23	22	adantrr	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to F : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (S)$
24		f1oco	$⊢ (G : ran 1^{st} (S) \underset{1-1 onto}{⟶} ran 1^{st} (T) \land F : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (S)) \to (G \circ F) : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (T)$
25	17 23 24	syl2anc	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to (G \circ F) : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (T)$
26	18 19 12 13	isrngoiso	$⊢ (R \in RingOps \land T \in RingOps) \to (G \circ F \in (R RingOpsIso T) \leftrightarrow (G \circ F \in (R RingOpsHom T) \land (G \circ F) : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (T)))$
27	26	3adant2	$⊢ (R \in RingOps \land S \in RingOps \land T \in RingOps) \to (G \circ F \in (R RingOpsIso T) \leftrightarrow (G \circ F \in (R RingOpsHom T) \land (G \circ F) : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (T)))$
28	27	adantr	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to (G \circ F \in (R RingOpsIso T) \leftrightarrow (G \circ F \in (R RingOpsHom T) \land (G \circ F) : ran 1^{st} (R) \underset{1-1 onto}{⟶} ran 1^{st} (T)))$
29	9 25 28	mpbir2and	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RingOpsIso S) \land G \in (S RingOpsIso T))) \to G \circ F \in (R RingOpsIso T)$

Metamath Proof Explorer

Theorem rngoisoco

Proof