Step | Hyp | Ref
| Expression |
1 | | rhmsscmap.r |
. . 3
⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) |
2 | | inss2 3796 |
. . 3
⊢ (Ring
∩ 𝑈) ⊆ 𝑈 |
3 | 1, 2 | syl6eqss 3618 |
. 2
⊢ (𝜑 → 𝑅 ⊆ 𝑈) |
4 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑎) =
(Base‘𝑎) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑏) =
(Base‘𝑏) |
6 | 4, 5 | rhmf 18549 |
. . . . . 6
⊢ (ℎ ∈ (𝑎 RingHom 𝑏) → ℎ:(Base‘𝑎)⟶(Base‘𝑏)) |
7 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ:(Base‘𝑎)⟶(Base‘𝑏)) |
8 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑏)
∈ V |
9 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑎)
∈ V |
10 | 8, 9 | pm3.2i 470 |
. . . . . . . . 9
⊢
((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) |
11 | | elmapg 7757 |
. . . . . . . . 9
⊢
(((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) → (ℎ ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)) ↔
ℎ:(Base‘𝑎)⟶(Base‘𝑏))) |
12 | 10, 11 | mp1i 13 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → (ℎ ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)) ↔
ℎ:(Base‘𝑎)⟶(Base‘𝑏))) |
13 | 7, 12 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) |
14 | 13 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (ℎ:(Base‘𝑎)⟶(Base‘𝑏) → ℎ ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)))) |
15 | 6, 14 | syl5 33 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (ℎ ∈ (𝑎 RingHom 𝑏) → ℎ ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)))) |
16 | 15 | ssrdv 3574 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎 RingHom 𝑏) ⊆ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) |
17 | | ovres 6698 |
. . . . 5
⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) = (𝑎 RingHom 𝑏)) |
18 | 17 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) = (𝑎 RingHom 𝑏)) |
19 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) |
20 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏)) |
21 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎)) |
22 | 20, 21 | oveqan12rd 6569 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((Base‘𝑦) ↑𝑚
(Base‘𝑥)) =
((Base‘𝑏)
↑𝑚 (Base‘𝑎))) |
23 | 22 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → ((Base‘𝑦) ↑𝑚
(Base‘𝑥)) =
((Base‘𝑏)
↑𝑚 (Base‘𝑎))) |
24 | 3 | sseld 3567 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 ∈ 𝑅 → 𝑎 ∈ 𝑈)) |
25 | 24 | com12 32 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑅 → (𝜑 → 𝑎 ∈ 𝑈)) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝜑 → 𝑎 ∈ 𝑈)) |
27 | 26 | impcom 445 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → 𝑎 ∈ 𝑈) |
28 | 3 | sseld 3567 |
. . . . . . . 8
⊢ (𝜑 → (𝑏 ∈ 𝑅 → 𝑏 ∈ 𝑈)) |
29 | 28 | com12 32 |
. . . . . . 7
⊢ (𝑏 ∈ 𝑅 → (𝜑 → 𝑏 ∈ 𝑈)) |
30 | 29 | adantl 481 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝜑 → 𝑏 ∈ 𝑈)) |
31 | 30 | impcom 445 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → 𝑏 ∈ 𝑈) |
32 | | ovex 6577 |
. . . . . 6
⊢
((Base‘𝑏)
↑𝑚 (Base‘𝑎)) ∈ V |
33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → ((Base‘𝑏) ↑𝑚
(Base‘𝑎)) ∈
V) |
34 | 19, 23, 27, 31, 33 | ovmpt2d 6686 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))𝑏) = ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) |
35 | 16, 18, 34 | 3sstr4d 3611 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))𝑏)) |
36 | 35 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑅 (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))𝑏)) |
37 | | rhmfn 41708 |
. . . . 5
⊢ RingHom
Fn (Ring × Ring) |
38 | 37 | a1i 11 |
. . . 4
⊢ (𝜑 → RingHom Fn (Ring ×
Ring)) |
39 | | inss1 3795 |
. . . . . 6
⊢ (Ring
∩ 𝑈) ⊆
Ring |
40 | 1, 39 | syl6eqss 3618 |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ Ring) |
41 | | xpss12 5148 |
. . . . 5
⊢ ((𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring) → (𝑅 × 𝑅) ⊆ (Ring ×
Ring)) |
42 | 40, 40, 41 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑅 × 𝑅) ⊆ (Ring ×
Ring)) |
43 | | fnssres 5918 |
. . . 4
⊢ ((
RingHom Fn (Ring × Ring) ∧ (𝑅 × 𝑅) ⊆ (Ring × Ring)) → (
RingHom ↾ (𝑅 ×
𝑅)) Fn (𝑅 × 𝑅)) |
44 | 38, 42, 43 | syl2anc 691 |
. . 3
⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅)) |
45 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) |
46 | | ovex 6577 |
. . . . 5
⊢
((Base‘𝑦)
↑𝑚 (Base‘𝑥)) ∈ V |
47 | 45, 46 | fnmpt2i 7128 |
. . . 4
⊢ (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) Fn (𝑈 × 𝑈) |
48 | 47 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) Fn (𝑈 × 𝑈)) |
49 | | rhmsscmap.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
50 | | elex 3185 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ V) |
51 | 49, 50 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ∈ V) |
52 | 44, 48, 51 | isssc 16303 |
. 2
⊢ (𝜑 → (( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) ↔
(𝑅 ⊆ 𝑈 ∧ ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑅 (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))𝑏)))) |
53 | 3, 36, 52 | mpbir2and 959 |
1
⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) |