| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . 7
⊢
(1st ‘𝑆) = (1st ‘𝑆) |
| 2 | | eqid 2737 |
. . . . . . 7
⊢ ran
(1st ‘𝑆) =
ran (1st ‘𝑆) |
| 3 | | eqid 2737 |
. . . . . . 7
⊢
(1st ‘𝑇) = (1st ‘𝑇) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢ ran
(1st ‘𝑇) =
ran (1st ‘𝑇) |
| 5 | 1, 2, 3, 4 | rngohomf 37973 |
. . . . . 6
⊢ ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → 𝐺:ran (1st ‘𝑆)⟶ran (1st
‘𝑇)) |
| 6 | 5 | 3expa 1119 |
. . . . 5
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → 𝐺:ran (1st ‘𝑆)⟶ran (1st
‘𝑇)) |
| 7 | 6 | 3adantl1 1167 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → 𝐺:ran (1st ‘𝑆)⟶ran (1st
‘𝑇)) |
| 8 | 7 | adantrl 716 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → 𝐺:ran (1st ‘𝑆)⟶ran (1st
‘𝑇)) |
| 9 | | eqid 2737 |
. . . . . . 7
⊢
(1st ‘𝑅) = (1st ‘𝑅) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) |
| 11 | 9, 10, 1, 2 | rngohomf 37973 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:ran (1st ‘𝑅)⟶ran (1st
‘𝑆)) |
| 12 | 11 | 3expa 1119 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:ran (1st ‘𝑅)⟶ran (1st
‘𝑆)) |
| 13 | 12 | 3adantl3 1169 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → 𝐹:ran (1st ‘𝑅)⟶ran (1st
‘𝑆)) |
| 14 | 13 | adantrr 717 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → 𝐹:ran (1st ‘𝑅)⟶ran (1st
‘𝑆)) |
| 15 | | fco 6760 |
. . 3
⊢ ((𝐺:ran (1st
‘𝑆)⟶ran
(1st ‘𝑇)
∧ 𝐹:ran (1st
‘𝑅)⟶ran
(1st ‘𝑆))
→ (𝐺 ∘ 𝐹):ran (1st
‘𝑅)⟶ran
(1st ‘𝑇)) |
| 16 | 8, 14, 15 | syl2anc 584 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹):ran (1st ‘𝑅)⟶ran (1st
‘𝑇)) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
| 18 | | eqid 2737 |
. . . . . . 7
⊢
(GId‘(2nd ‘𝑅)) = (GId‘(2nd ‘𝑅)) |
| 19 | 10, 17, 18 | rngo1cl 37946 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
(GId‘(2nd ‘𝑅)) ∈ ran (1st ‘𝑅)) |
| 20 | 19 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) →
(GId‘(2nd ‘𝑅)) ∈ ran (1st ‘𝑅)) |
| 21 | 20 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (GId‘(2nd
‘𝑅)) ∈ ran
(1st ‘𝑅)) |
| 22 | | fvco3 7008 |
. . . 4
⊢ ((𝐹:ran (1st
‘𝑅)⟶ran
(1st ‘𝑆)
∧ (GId‘(2nd ‘𝑅)) ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘(GId‘(2nd
‘𝑅))) = (𝐺‘(𝐹‘(GId‘(2nd
‘𝑅))))) |
| 23 | 14, 21, 22 | syl2anc 584 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → ((𝐺 ∘ 𝐹)‘(GId‘(2nd
‘𝑅))) = (𝐺‘(𝐹‘(GId‘(2nd
‘𝑅))))) |
| 24 | | eqid 2737 |
. . . . . . . . 9
⊢
(2nd ‘𝑆) = (2nd ‘𝑆) |
| 25 | | eqid 2737 |
. . . . . . . . 9
⊢
(GId‘(2nd ‘𝑆)) = (GId‘(2nd ‘𝑆)) |
| 26 | 17, 18, 24, 25 | rngohom1 37975 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑆))) |
| 27 | 26 | 3expa 1119 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑆))) |
| 28 | 27 | 3adantl3 1169 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (𝐹‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑆))) |
| 29 | 28 | adantrr 717 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐹‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑆))) |
| 30 | 29 | fveq2d 6910 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺‘(𝐹‘(GId‘(2nd
‘𝑅)))) = (𝐺‘(GId‘(2nd
‘𝑆)))) |
| 31 | | eqid 2737 |
. . . . . . . 8
⊢
(2nd ‘𝑇) = (2nd ‘𝑇) |
| 32 | | eqid 2737 |
. . . . . . . 8
⊢
(GId‘(2nd ‘𝑇)) = (GId‘(2nd ‘𝑇)) |
| 33 | 24, 25, 31, 32 | rngohom1 37975 |
. . . . . . 7
⊢ ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (𝐺‘(GId‘(2nd
‘𝑆))) =
(GId‘(2nd ‘𝑇))) |
| 34 | 33 | 3expa 1119 |
. . . . . 6
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (𝐺‘(GId‘(2nd
‘𝑆))) =
(GId‘(2nd ‘𝑇))) |
| 35 | 34 | 3adantl1 1167 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (𝐺‘(GId‘(2nd
‘𝑆))) =
(GId‘(2nd ‘𝑇))) |
| 36 | 35 | adantrl 716 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺‘(GId‘(2nd
‘𝑆))) =
(GId‘(2nd ‘𝑇))) |
| 37 | 30, 36 | eqtrd 2777 |
. . 3
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺‘(𝐹‘(GId‘(2nd
‘𝑅)))) =
(GId‘(2nd ‘𝑇))) |
| 38 | 23, 37 | eqtrd 2777 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → ((𝐺 ∘ 𝐹)‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑇))) |
| 39 | 9, 10, 1 | rngohomadd 37976 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) |
| 40 | 39 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)))) |
| 41 | 40 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)))) |
| 42 | 41 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)))) |
| 43 | 42 | imp 406 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) |
| 44 | 43 | adantlrr 721 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(1st ‘𝑅)𝑦)) = ((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) |
| 45 | 44 | fveq2d 6910 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐺‘(𝐹‘(𝑥(1st ‘𝑅)𝑦))) = (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦)))) |
| 46 | 9, 10, 1, 2 | rngohomcl 37974 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝑥 ∈ ran (1st ‘𝑅)) → (𝐹‘𝑥) ∈ ran (1st ‘𝑆)) |
| 47 | 9, 10, 1, 2 | rngohomcl 37974 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) |
| 48 | 46, 47 | anim12dan 619 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) |
| 49 | 48 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)))) |
| 50 | 49 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)))) |
| 51 | 50 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)))) |
| 52 | 51 | imp 406 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) |
| 53 | 52 | adantlrr 721 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) |
| 54 | 1, 2, 3 | rngohomadd 37976 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 55 | 54 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦))))) |
| 56 | 55 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦))))) |
| 57 | 56 | 3adantl1 1167 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦))))) |
| 58 | 57 | imp 406 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 59 | 58 | adantlrl 720 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 60 | 53, 59 | syldan 591 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐺‘((𝐹‘𝑥)(1st ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 61 | 45, 60 | eqtrd 2777 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐺‘(𝐹‘(𝑥(1st ‘𝑅)𝑦))) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 62 | 9, 10 | rngogcl 37919 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅)) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 63 | 62 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅))) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 64 | 63 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅))) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 65 | 64 | adantlr 715 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 66 | | fvco3 7008 |
. . . . . . 7
⊢ ((𝐹:ran (1st
‘𝑅)⟶ran
(1st ‘𝑆)
∧ (𝑥(1st
‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st ‘𝑅)𝑦)))) |
| 67 | 14, 66 | sylan 580 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥(1st ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st ‘𝑅)𝑦)))) |
| 68 | 65, 67 | syldan 591 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(1st ‘𝑅)𝑦)))) |
| 69 | | fvco3 7008 |
. . . . . . . 8
⊢ ((𝐹:ran (1st
‘𝑅)⟶ran
(1st ‘𝑆)
∧ 𝑥 ∈ ran
(1st ‘𝑅))
→ ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
| 70 | 14, 69 | sylan 580 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ 𝑥 ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
| 71 | | fvco3 7008 |
. . . . . . . 8
⊢ ((𝐹:ran (1st
‘𝑅)⟶ran
(1st ‘𝑆)
∧ 𝑦 ∈ ran
(1st ‘𝑅))
→ ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦))) |
| 72 | 14, 71 | sylan 580 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦))) |
| 73 | 70, 72 | anim12dan 619 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)) ∧ ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦)))) |
| 74 | | oveq12 7440 |
. . . . . 6
⊢ ((((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)) ∧ ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦))) → (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 75 | 73, 74 | syl 17 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) = ((𝐺‘(𝐹‘𝑥))(1st ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 76 | 61, 68, 75 | 3eqtr4d 2787 |
. . . 4
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦))) |
| 77 | 9, 10, 17, 24 | rngohommul 37977 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) |
| 78 | 77 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))) |
| 79 | 78 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))) |
| 80 | 79 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → ((𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅)) → (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))) |
| 81 | 80 | imp 406 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) |
| 82 | 81 | adantlrr 721 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐹‘(𝑥(2nd ‘𝑅)𝑦)) = ((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) |
| 83 | 82 | fveq2d 6910 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐺‘(𝐹‘(𝑥(2nd ‘𝑅)𝑦))) = (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦)))) |
| 84 | 1, 2, 24, 31 | rngohommul 37977 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 85 | 84 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦))))) |
| 86 | 85 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦))))) |
| 87 | 86 | 3adantl1 1167 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) → (((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆)) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦))))) |
| 88 | 87 | imp 406 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 89 | 88 | adantlrl 720 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ ((𝐹‘𝑥) ∈ ran (1st ‘𝑆) ∧ (𝐹‘𝑦) ∈ ran (1st ‘𝑆))) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 90 | 53, 89 | syldan 591 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐺‘((𝐹‘𝑥)(2nd ‘𝑆)(𝐹‘𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 91 | 83, 90 | eqtrd 2777 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝐺‘(𝐹‘(𝑥(2nd ‘𝑅)𝑦))) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 92 | 9, 17, 10 | rngocl 37908 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅)) → (𝑥(2nd ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 93 | 92 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅))) → (𝑥(2nd ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 94 | 93 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅))) → (𝑥(2nd ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 95 | 94 | adantlr 715 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) |
| 96 | | fvco3 7008 |
. . . . . . 7
⊢ ((𝐹:ran (1st
‘𝑅)⟶ran
(1st ‘𝑆)
∧ (𝑥(2nd
‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd ‘𝑅)𝑦)))) |
| 97 | 14, 96 | sylan 580 |
. . . . . 6
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥(2nd ‘𝑅)𝑦) ∈ ran (1st ‘𝑅)) → ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd ‘𝑅)𝑦)))) |
| 98 | 95, 97 | syldan 591 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (𝐺‘(𝐹‘(𝑥(2nd ‘𝑅)𝑦)))) |
| 99 | | oveq12 7440 |
. . . . . 6
⊢ ((((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥)) ∧ ((𝐺 ∘ 𝐹)‘𝑦) = (𝐺‘(𝐹‘𝑦))) → (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 100 | 73, 99 | syl 17 |
. . . . 5
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) = ((𝐺‘(𝐹‘𝑥))(2nd ‘𝑇)(𝐺‘(𝐹‘𝑦)))) |
| 101 | 91, 98, 100 | 3eqtr4d 2787 |
. . . 4
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦))) |
| 102 | 76, 101 | jca 511 |
. . 3
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (𝑥 ∈ ran (1st ‘𝑅) ∧ 𝑦 ∈ ran (1st ‘𝑅))) → (((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) ∧ ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)))) |
| 103 | 102 | ralrimivva 3202 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)(((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) ∧ ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)))) |
| 104 | 9, 17, 10, 18, 3, 31, 4, 32 | isrngohom 37972 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st ‘𝑅)⟶ran (1st
‘𝑇) ∧ ((𝐺 ∘ 𝐹)‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑇)) ∧ ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)(((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) ∧ ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)))))) |
| 105 | 104 | 3adant2 1132 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) → ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st ‘𝑅)⟶ran (1st
‘𝑇) ∧ ((𝐺 ∘ 𝐹)‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑇)) ∧ ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)(((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) ∧ ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)))))) |
| 106 | 105 | adantr 480 |
. 2
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st ‘𝑅)⟶ran (1st
‘𝑇) ∧ ((𝐺 ∘ 𝐹)‘(GId‘(2nd
‘𝑅))) =
(GId‘(2nd ‘𝑇)) ∧ ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)(((𝐺 ∘ 𝐹)‘(𝑥(1st ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(1st ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)) ∧ ((𝐺 ∘ 𝐹)‘(𝑥(2nd ‘𝑅)𝑦)) = (((𝐺 ∘ 𝐹)‘𝑥)(2nd ‘𝑇)((𝐺 ∘ 𝐹)‘𝑦)))))) |
| 107 | 16, 38, 103, 106 | mpbir3and 1343 |
1
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) → (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇)) |