Step | Hyp | Ref
| Expression |
1 | | evlsval.q |
. . . 4
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) |
2 | | evlsval.w |
. . . 4
⊢ 𝑊 = (𝐼 mPoly 𝑈) |
3 | | evlsval.v |
. . . 4
⊢ 𝑉 = (𝐼 mVar 𝑈) |
4 | | evlsval.u |
. . . 4
⊢ 𝑈 = (𝑆 ↾s 𝑅) |
5 | | evlsval.t |
. . . 4
⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑𝑚
𝐼)) |
6 | | evlsval.b |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
7 | | evlsval.a |
. . . 4
⊢ 𝐴 = (algSc‘𝑊) |
8 | | evlsval.x |
. . . 4
⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) |
9 | | evlsval.y |
. . . 4
⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | evlsval 19991 |
. . 3
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌))) |
11 | | eqid 2795 |
. . . . 5
⊢
(Base‘𝑇) =
(Base‘𝑇) |
12 | | elex 3455 |
. . . . . 6
⊢ (𝐼 ∈ 𝑍 → 𝐼 ∈ V) |
13 | 12 | 3ad2ant1 1126 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝐼 ∈ V) |
14 | 4 | subrgcrng 19234 |
. . . . . 6
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) |
15 | 14 | 3adant1 1123 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) |
16 | | simp2 1130 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑆 ∈ CRing) |
17 | | ovex 7053 |
. . . . . 6
⊢ (𝐵 ↑𝑚
𝐼) ∈
V |
18 | 5 | pwscrng 19062 |
. . . . . 6
⊢ ((𝑆 ∈ CRing ∧ (𝐵 ↑𝑚
𝐼) ∈ V) → 𝑇 ∈ CRing) |
19 | 16, 17, 18 | sylancl 586 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑇 ∈ CRing) |
20 | 6 | subrgss 19231 |
. . . . . . . . 9
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐵) |
21 | 20 | 3ad2ant3 1128 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑅 ⊆ 𝐵) |
22 | 21 | resmptd 5794 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥}))) |
23 | 22, 8 | syl6eqr 2849 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) = 𝑋) |
24 | | crngring 19003 |
. . . . . . . . 9
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
25 | 24 | 3ad2ant2 1127 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑆 ∈ Ring) |
26 | | eqid 2795 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) = (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) |
27 | 5, 6, 26 | pwsdiagrhm 19264 |
. . . . . . . 8
⊢ ((𝑆 ∈ Ring ∧ (𝐵 ↑𝑚
𝐼) ∈ V) → (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇)) |
28 | 25, 17, 27 | sylancl 586 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇)) |
29 | | simp3 1131 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑅 ∈ (SubRing‘𝑆)) |
30 | 4 | resrhm 19259 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇) ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) ∈ (𝑈 RingHom 𝑇)) |
31 | 28, 29, 30 | syl2anc 584 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) ∈ (𝑈 RingHom 𝑇)) |
32 | 23, 31 | eqeltrrd 2884 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑋 ∈ (𝑈 RingHom 𝑇)) |
33 | 6 | fvexi 6557 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
34 | | simpl1 1184 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑍) |
35 | | elmapg 8274 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ 𝐼 ∈ 𝑍) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↔ 𝑔:𝐼⟶𝐵)) |
36 | 33, 34, 35 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↔ 𝑔:𝐼⟶𝐵)) |
37 | 36 | biimpa 477 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑔:𝐼⟶𝐵) |
38 | | simplr 765 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑥 ∈ 𝐼) |
39 | 37, 38 | ffvelrnd 6722 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) → (𝑔‘𝑥) ∈ 𝐵) |
40 | 39 | fmpttd 6747 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)):(𝐵 ↑𝑚 𝐼)⟶𝐵) |
41 | | simpl2 1185 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing) |
42 | 5, 6, 11 | pwselbasb 16595 |
. . . . . . . 8
⊢ ((𝑆 ∈ CRing ∧ (𝐵 ↑𝑚
𝐼) ∈ V) → ((𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) ∈ (Base‘𝑇) ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)):(𝐵 ↑𝑚 𝐼)⟶𝐵)) |
43 | 41, 17, 42 | sylancl 586 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → ((𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) ∈ (Base‘𝑇) ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)):(𝐵 ↑𝑚 𝐼)⟶𝐵)) |
44 | 40, 43 | mpbird 258 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) ∈ (Base‘𝑇)) |
45 | 44, 9 | fmptd 6746 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑌:𝐼⟶(Base‘𝑇)) |
46 | 2, 11, 7, 3, 13, 15, 19, 32, 45 | evlseu 19988 |
. . . 4
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ∃!𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)) |
47 | | riotacl2 6995 |
. . . 4
⊢
(∃!𝑚 ∈
(𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌) → (℩𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)) ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)}) |
48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (℩𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)) ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)}) |
49 | 10, 48 | eqeltrd 2883 |
. 2
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)}) |
50 | | coeq1 5619 |
. . . . 5
⊢ (𝑚 = 𝑄 → (𝑚 ∘ 𝐴) = (𝑄 ∘ 𝐴)) |
51 | 50 | eqeq1d 2797 |
. . . 4
⊢ (𝑚 = 𝑄 → ((𝑚 ∘ 𝐴) = 𝑋 ↔ (𝑄 ∘ 𝐴) = 𝑋)) |
52 | | coeq1 5619 |
. . . . 5
⊢ (𝑚 = 𝑄 → (𝑚 ∘ 𝑉) = (𝑄 ∘ 𝑉)) |
53 | 52 | eqeq1d 2797 |
. . . 4
⊢ (𝑚 = 𝑄 → ((𝑚 ∘ 𝑉) = 𝑌 ↔ (𝑄 ∘ 𝑉) = 𝑌)) |
54 | 51, 53 | anbi12d 630 |
. . 3
⊢ (𝑚 = 𝑄 → (((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌) ↔ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌))) |
55 | 54 | elrab 3619 |
. 2
⊢ (𝑄 ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)} ↔ (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌))) |
56 | 49, 55 | sylib 219 |
1
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌))) |