rngoisoco

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

		Ref	Expression
	Assertion	rngoisoco	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngIso 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		rngoisohom	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) )
2	1	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) )
3	2	3adantl3	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) )
4		rngoisohom	⊢ ( ( 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) → 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) )
5	4	3expa	⊢ ( ( ( 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) → 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) )
6	5	3adantl1	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) → 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) )
7	3 6	anim12dan	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) ) )
8		rngohomco	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngHom 𝑇 ) )
9	7 8	syldan	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngHom 𝑇 ) )
10		eqid	⊢ ( 1^st ‘ 𝑆 ) = ( 1^st ‘ 𝑆 )
11		eqid	⊢ ran ( 1^st ‘ 𝑆 ) = ran ( 1^st ‘ 𝑆 )
12		eqid	⊢ ( 1^st ‘ 𝑇 ) = ( 1^st ‘ 𝑇 )
13		eqid	⊢ ran ( 1^st ‘ 𝑇 ) = ran ( 1^st ‘ 𝑇 )
14	10 11 12 13	rngoiso1o	⊢ ( ( 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) → 𝐺 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) )
15	14	3expa	⊢ ( ( ( 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) → 𝐺 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) )
16	15	3adantl1	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) → 𝐺 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) )
17	16	adantrl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → 𝐺 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) )
18		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
19		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
20	18 19 10 11	rngoiso1o	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) )
21	20	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) )
22	21	3adantl3	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) )
23	22	adantrr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) )
24		f1oco	⊢ ( ( 𝐺 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐺 ∘ 𝐹 ) : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) )
25	17 23 24	syl2anc	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → ( 𝐺 ∘ 𝐹 ) : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) )
26	18 19 12 13	isrngoiso	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngIso 𝑇 ) ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngHom 𝑇 ) ∧ ( 𝐺 ∘ 𝐹 ) : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) ) ) )
27	26	3adant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngIso 𝑇 ) ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngHom 𝑇 ) ∧ ( 𝐺 ∘ 𝐹 ) : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) ) ) )
28	27	adantr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngIso 𝑇 ) ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngHom 𝑇 ) ∧ ( 𝐺 ∘ 𝐹 ) : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑇 ) ) ) )
29	9 25 28	mpbir2and	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngIso 𝑇 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝑅 RngIso 𝑇 ) )

Metamath Proof Explorer

Theorem rngoisoco

Proof