Proof of Theorem rhmsubclem4
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → 𝜑) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝜑) |
| 3 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝑅) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑅) |
| 5 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝑦 ∈ 𝑅) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑅) |
| 7 | | rngcrescrhm.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 8 | | rngcrescrhm.c |
. . . . . . . 8
⊢ 𝐶 = (RngCat‘𝑈) |
| 9 | | rngcrescrhm.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) |
| 10 | | rngcrescrhm.h |
. . . . . . . 8
⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) |
| 11 | 7, 8, 9, 10 | rhmsubclem2 20686 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝑥𝐻𝑦) = (𝑥 RingHom 𝑦)) |
| 12 | 2, 4, 6, 11 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑥𝐻𝑦) = (𝑥 RingHom 𝑦)) |
| 13 | 12 | eleq2d 2827 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑥 RingHom 𝑦))) |
| 14 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ 𝑅) |
| 15 | 14 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑅) |
| 16 | 7, 8, 9, 10 | rhmsubclem2 20686 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → (𝑦𝐻𝑧) = (𝑦 RingHom 𝑧)) |
| 17 | 2, 6, 15, 16 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑦𝐻𝑧) = (𝑦 RingHom 𝑧)) |
| 18 | 17 | eleq2d 2827 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦 RingHom 𝑧))) |
| 19 | 13, 18 | anbi12d 632 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) ↔ (𝑓 ∈ (𝑥 RingHom 𝑦) ∧ 𝑔 ∈ (𝑦 RingHom 𝑧)))) |
| 20 | | rhmco 20501 |
. . . . 5
⊢ ((𝑔 ∈ (𝑦 RingHom 𝑧) ∧ 𝑓 ∈ (𝑥 RingHom 𝑦)) → (𝑔 ∘ 𝑓) ∈ (𝑥 RingHom 𝑧)) |
| 21 | 20 | ancoms 458 |
. . . 4
⊢ ((𝑓 ∈ (𝑥 RingHom 𝑦) ∧ 𝑔 ∈ (𝑦 RingHom 𝑧)) → (𝑔 ∘ 𝑓) ∈ (𝑥 RingHom 𝑧)) |
| 22 | 19, 21 | biimtrdi 253 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (𝑔 ∘ 𝑓) ∈ (𝑥 RingHom 𝑧))) |
| 23 | 22 | imp 406 |
. 2
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔 ∘ 𝑓) ∈ (𝑥 RingHom 𝑧)) |
| 24 | 7 | ad3antrrr 730 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → 𝑈 ∈ 𝑉) |
| 25 | 8 | eqcomi 2746 |
. . . 4
⊢
(RngCat‘𝑈) =
𝐶 |
| 26 | 25 | fveq2i 6909 |
. . 3
⊢
(comp‘(RngCat‘𝑈)) = (comp‘𝐶) |
| 27 | | inss2 4238 |
. . . . . . 7
⊢ (Ring
∩ 𝑈) ⊆ 𝑈 |
| 28 | 9, 27 | eqsstrdi 4028 |
. . . . . 6
⊢ (𝜑 → 𝑅 ⊆ 𝑈) |
| 29 | 28 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → 𝑥 ∈ 𝑈) |
| 30 | 29 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑥 ∈ 𝑈) |
| 31 | 30 | adantr 480 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → 𝑥 ∈ 𝑈) |
| 32 | 28 | sseld 3982 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑅 → 𝑦 ∈ 𝑈)) |
| 33 | 32 | adantrd 491 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝑦 ∈ 𝑈)) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝑦 ∈ 𝑈)) |
| 35 | 34 | imp 406 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑦 ∈ 𝑈) |
| 36 | 35 | adantr 480 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → 𝑦 ∈ 𝑈) |
| 37 | 28 | sseld 3982 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑈)) |
| 38 | 37 | adantld 490 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ 𝑈)) |
| 39 | 38 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝑧 ∈ 𝑈)) |
| 40 | 39 | imp 406 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑧 ∈ 𝑈) |
| 41 | 40 | adantr 480 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → 𝑧 ∈ 𝑈) |
| 42 | 10 | oveqi 7444 |
. . . . . . . . 9
⊢ (𝑥𝐻𝑦) = (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) |
| 43 | 4, 6 | ovresd 7600 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) = (𝑥 RingHom 𝑦)) |
| 44 | 42, 43 | eqtrid 2789 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑥𝐻𝑦) = (𝑥 RingHom 𝑦)) |
| 45 | 44 | eleq2d 2827 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑥 RingHom 𝑦))) |
| 46 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑥) =
(Base‘𝑥) |
| 47 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑦) =
(Base‘𝑦) |
| 48 | 46, 47 | rhmf 20485 |
. . . . . . 7
⊢ (𝑓 ∈ (𝑥 RingHom 𝑦) → 𝑓:(Base‘𝑥)⟶(Base‘𝑦)) |
| 49 | 45, 48 | biimtrdi 253 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑓 ∈ (𝑥𝐻𝑦) → 𝑓:(Base‘𝑥)⟶(Base‘𝑦))) |
| 50 | 49 | com12 32 |
. . . . 5
⊢ (𝑓 ∈ (𝑥𝐻𝑦) → (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑓:(Base‘𝑥)⟶(Base‘𝑦))) |
| 51 | 50 | adantr 480 |
. . . 4
⊢ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑓:(Base‘𝑥)⟶(Base‘𝑦))) |
| 52 | 51 | impcom 407 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → 𝑓:(Base‘𝑥)⟶(Base‘𝑦)) |
| 53 | 10 | oveqi 7444 |
. . . . . . . . 9
⊢ (𝑦𝐻𝑧) = (𝑦( RingHom ↾ (𝑅 × 𝑅))𝑧) |
| 54 | | ovres 7599 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → (𝑦( RingHom ↾ (𝑅 × 𝑅))𝑧) = (𝑦 RingHom 𝑧)) |
| 55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑦( RingHom ↾ (𝑅 × 𝑅))𝑧) = (𝑦 RingHom 𝑧)) |
| 56 | 53, 55 | eqtrid 2789 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑦𝐻𝑧) = (𝑦 RingHom 𝑧)) |
| 57 | 56 | eleq2d 2827 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦 RingHom 𝑧))) |
| 58 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑧) =
(Base‘𝑧) |
| 59 | 47, 58 | rhmf 20485 |
. . . . . . 7
⊢ (𝑔 ∈ (𝑦 RingHom 𝑧) → 𝑔:(Base‘𝑦)⟶(Base‘𝑧)) |
| 60 | 57, 59 | biimtrdi 253 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑔 ∈ (𝑦𝐻𝑧) → 𝑔:(Base‘𝑦)⟶(Base‘𝑧))) |
| 61 | 60 | com12 32 |
. . . . 5
⊢ (𝑔 ∈ (𝑦𝐻𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑔:(Base‘𝑦)⟶(Base‘𝑧))) |
| 62 | 61 | adantl 481 |
. . . 4
⊢ ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧)) → (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → 𝑔:(Base‘𝑦)⟶(Base‘𝑧))) |
| 63 | 62 | impcom 407 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → 𝑔:(Base‘𝑦)⟶(Base‘𝑧)) |
| 64 | 8, 24, 26, 31, 36, 41, 52, 63 | rngcco 20627 |
. 2
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCat‘𝑈))𝑧)𝑓) = (𝑔 ∘ 𝑓)) |
| 65 | 7, 8, 9, 10 | rhmsubclem2 20686 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → (𝑥𝐻𝑧) = (𝑥 RingHom 𝑧)) |
| 66 | 2, 4, 15, 65 | syl3anc 1373 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) → (𝑥𝐻𝑧) = (𝑥 RingHom 𝑧)) |
| 67 | 66 | adantr 480 |
. 2
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑥𝐻𝑧) = (𝑥 RingHom 𝑧)) |
| 68 | 23, 64, 67 | 3eltr4d 2856 |
1
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |