Step | Hyp | Ref
| Expression |
1 | | ringrng 41879 |
. . . . . 6
⊢ (𝑟 ∈ Ring → 𝑟 ∈ Rng) |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑟 ∈ Ring → 𝑟 ∈ Rng)) |
3 | 2 | ssrdv 3609 |
. . . 4
⊢ (𝜑 → Ring ⊆
Rng) |
4 | | ssrin 3838 |
. . . 4
⊢ (Ring
⊆ Rng → (Ring ∩ 𝑈) ⊆ (Rng ∩ 𝑈)) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → (Ring ∩ 𝑈) ⊆ (Rng ∩ 𝑈)) |
6 | | rhmsscrnghm.r |
. . 3
⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) |
7 | | rhmsscrnghm.s |
. . 3
⊢ (𝜑 → 𝑆 = (Rng ∩ 𝑈)) |
8 | 5, 6, 7 | 3sstr4d 3648 |
. 2
⊢ (𝜑 → 𝑅 ⊆ 𝑆) |
9 | | ovres 6800 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) = (𝑥 RingHom 𝑦)) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) = (𝑥 RingHom 𝑦)) |
11 | 10 | eleq2d 2687 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ↔ ℎ ∈ (𝑥 RingHom 𝑦))) |
12 | | rhmisrnghm 41920 |
. . . . . 6
⊢ (ℎ ∈ (𝑥 RingHom 𝑦) → ℎ ∈ (𝑥 RngHomo 𝑦)) |
13 | 8 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑅 → 𝑥 ∈ 𝑆)) |
14 | 8 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝑅 → 𝑦 ∈ 𝑆)) |
15 | 13, 14 | anim12d 586 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆))) |
16 | 15 | imp 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) |
17 | | ovres 6800 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦) = (𝑥 RngHomo 𝑦)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦) = (𝑥 RngHomo 𝑦)) |
19 | 18 | eleq2d 2687 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦) ↔ ℎ ∈ (𝑥 RngHomo 𝑦))) |
20 | 12, 19 | syl5ibr 236 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥 RingHom 𝑦) → ℎ ∈ (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦))) |
21 | 11, 20 | sylbid 230 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (ℎ ∈ (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) → ℎ ∈ (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦))) |
22 | 21 | ssrdv 3609 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ⊆ (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦)) |
23 | 22 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ⊆ (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦)) |
24 | | inss1 3833 |
. . . . . 6
⊢ (Ring
∩ 𝑈) ⊆
Ring |
25 | 6, 24 | syl6eqss 3655 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ Ring) |
26 | | xpss12 5225 |
. . . . 5
⊢ ((𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring) → (𝑅 × 𝑅) ⊆ (Ring ×
Ring)) |
27 | 25, 25, 26 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑅 × 𝑅) ⊆ (Ring ×
Ring)) |
28 | | rhmfn 41918 |
. . . . 5
⊢ RingHom
Fn (Ring × Ring) |
29 | | fnssresb 6003 |
. . . . 5
⊢ ( RingHom
Fn (Ring × Ring) → (( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅) ↔ (𝑅 × 𝑅) ⊆ (Ring ×
Ring))) |
30 | 28, 29 | mp1i 13 |
. . . 4
⊢ (𝜑 → (( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅) ↔ (𝑅 × 𝑅) ⊆ (Ring ×
Ring))) |
31 | 27, 30 | mpbird 247 |
. . 3
⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅)) |
32 | | inss1 3833 |
. . . . . 6
⊢ (Rng
∩ 𝑈) ⊆
Rng |
33 | 7, 32 | syl6eqss 3655 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ Rng) |
34 | | xpss12 5225 |
. . . . 5
⊢ ((𝑆 ⊆ Rng ∧ 𝑆 ⊆ Rng) → (𝑆 × 𝑆) ⊆ (Rng ×
Rng)) |
35 | 33, 33, 34 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑆 × 𝑆) ⊆ (Rng ×
Rng)) |
36 | | rnghmfn 41890 |
. . . . 5
⊢ RngHomo
Fn (Rng × Rng) |
37 | | fnssresb 6003 |
. . . . 5
⊢ ( RngHomo
Fn (Rng × Rng) → (( RngHomo ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆) ↔ (𝑆 × 𝑆) ⊆ (Rng ×
Rng))) |
38 | 36, 37 | mp1i 13 |
. . . 4
⊢ (𝜑 → (( RngHomo ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆) ↔ (𝑆 × 𝑆) ⊆ (Rng ×
Rng))) |
39 | 35, 38 | mpbird 247 |
. . 3
⊢ (𝜑 → ( RngHomo ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆)) |
40 | | rhmsscrnghm.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
41 | | incom 3805 |
. . . . . 6
⊢ (Rng
∩ 𝑈) = (𝑈 ∩ Rng) |
42 | | inex1g 4801 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Rng) ∈ V) |
43 | 41, 42 | syl5eqel 2705 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → (Rng ∩ 𝑈) ∈ V) |
44 | 40, 43 | syl 17 |
. . . 4
⊢ (𝜑 → (Rng ∩ 𝑈) ∈ V) |
45 | 7, 44 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
46 | 31, 39, 45 | isssc 16480 |
. 2
⊢ (𝜑 → (( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHomo ↾
(𝑆 × 𝑆)) ↔ (𝑅 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝑥( RingHom ↾ (𝑅 × 𝑅))𝑦) ⊆ (𝑥( RngHomo ↾ (𝑆 × 𝑆))𝑦)))) |
47 | 8, 23, 46 | mpbir2and 957 |
1
⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat ( RngHomo ↾
(𝑆 × 𝑆))) |