Proof of Theorem rngoisoco
| Step | Hyp | Ref
| Expression |
| 1 | | rngoisohom 37987 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) |
| 2 | 1 | 3expa 1119 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) |
| 3 | 2 | 3adantl3 1169 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) |
| 4 | | rngoisohom 37987 |
. . . . . 6
⊢ ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇)) → 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) |
| 5 | 4 | 3expa 1119 |
. . . . 5
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇)) → 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) |
| 6 | 5 | 3adantl1 1167 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇)) → 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) |
| 7 | 3, 6 | anim12dan 619 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) |
| 8 | | rngohomco 37981 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇)) |
| 9 | 7, 8 | syldan 591 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇)) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢
(1st ‘𝑆) = (1st ‘𝑆) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢ ran
(1st ‘𝑆) =
ran (1st ‘𝑆) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢
(1st ‘𝑇) = (1st ‘𝑇) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢ ran
(1st ‘𝑇) =
ran (1st ‘𝑇) |
| 14 | 10, 11, 12, 13 | rngoiso1o 37986 |
. . . . . 6
⊢ ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇)) → 𝐺:ran (1st ‘𝑆)–1-1-onto→ran
(1st ‘𝑇)) |
| 15 | 14 | 3expa 1119 |
. . . . 5
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇)) → 𝐺:ran (1st ‘𝑆)–1-1-onto→ran
(1st ‘𝑇)) |
| 16 | 15 | 3adantl1 1167 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇)) → 𝐺:ran (1st ‘𝑆)–1-1-onto→ran
(1st ‘𝑇)) |
| 17 | 16 | adantrl 716 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → 𝐺:ran (1st ‘𝑆)–1-1-onto→ran
(1st ‘𝑇)) |
| 18 | | eqid 2737 |
. . . . . . 7
⊢
(1st ‘𝑅) = (1st ‘𝑅) |
| 19 | | eqid 2737 |
. . . . . . 7
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) |
| 20 | 18, 19, 10, 11 | rngoiso1o 37986 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑆)) |
| 21 | 20 | 3expa 1119 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑆)) |
| 22 | 21 | 3adantl3 1169 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsIso 𝑆)) → 𝐹:ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑆)) |
| 23 | 22 | adantrr 717 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → 𝐹:ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑆)) |
| 24 | | f1oco 6871 |
. . 3
⊢ ((𝐺:ran (1st
‘𝑆)–1-1-onto→ran (1st ‘𝑇) ∧ 𝐹:ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑆))
→ (𝐺 ∘ 𝐹):ran (1st
‘𝑅)–1-1-onto→ran (1st ‘𝑇)) |
| 25 | 17, 23, 24 | syl2anc 584 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐺 ∘ 𝐹):ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑇)) |
| 26 | 18, 19, 12, 13 | isrngoiso 37985 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇) ↔ ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ∧ (𝐺 ∘ 𝐹):ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑇)))) |
| 27 | 26 | 3adant2 1132 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇) ↔ ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ∧ (𝐺 ∘ 𝐹):ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑇)))) |
| 28 | 27 | adantr 480 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇) ↔ ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ∧ (𝐺 ∘ 𝐹):ran (1st ‘𝑅)–1-1-onto→ran
(1st ‘𝑇)))) |
| 29 | 9, 25, 28 | mpbir2and 713 |
1
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsIso 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsIso 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsIso 𝑇)) |