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 19519 |
. . 3
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌))) |
11 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑇) =
(Base‘𝑇) |
12 | | elex 3212 |
. . . . . 6
⊢ (𝐼 ∈ 𝑍 → 𝐼 ∈ V) |
13 | 12 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝐼 ∈ V) |
14 | 4 | subrgcrng 18784 |
. . . . . 6
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) |
15 | 14 | 3adant1 1079 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) |
16 | | simp2 1062 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑆 ∈ CRing) |
17 | | ovex 6678 |
. . . . . 6
⊢ (𝐵 ↑𝑚
𝐼) ∈
V |
18 | 5 | pwscrng 18617 |
. . . . . 6
⊢ ((𝑆 ∈ CRing ∧ (𝐵 ↑𝑚
𝐼) ∈ V) → 𝑇 ∈ CRing) |
19 | 16, 17, 18 | sylancl 694 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑇 ∈ CRing) |
20 | 6 | subrgss 18781 |
. . . . . . . . 9
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐵) |
21 | 20 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑅 ⊆ 𝐵) |
22 | 21 | resmptd 5452 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥}))) |
23 | 22, 8 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) = 𝑋) |
24 | | crngring 18558 |
. . . . . . . . 9
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
25 | 24 | 3ad2ant2 1083 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑆 ∈ Ring) |
26 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) = (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) |
27 | 5, 6, 26 | pwsdiagrhm 18813 |
. . . . . . . 8
⊢ ((𝑆 ∈ Ring ∧ (𝐵 ↑𝑚
𝐼) ∈ V) → (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇)) |
28 | 25, 17, 27 | sylancl 694 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇)) |
29 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑅 ∈ (SubRing‘𝑆)) |
30 | 4 | resrhm 18809 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ∈ (𝑆 RingHom 𝑇) ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) ∈ (𝑈 RingHom 𝑇)) |
31 | 28, 29, 30 | syl2anc 693 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑥 ∈ 𝐵 ↦ ((𝐵 ↑𝑚 𝐼) × {𝑥})) ↾ 𝑅) ∈ (𝑈 RingHom 𝑇)) |
32 | 23, 31 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑋 ∈ (𝑈 RingHom 𝑇)) |
33 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(Base‘𝑆)
∈ V |
34 | 6, 33 | eqeltri 2697 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
35 | | simpl1 1064 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑍) |
36 | | elmapg 7870 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ 𝐼 ∈ 𝑍) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↔ 𝑔:𝐼⟶𝐵)) |
37 | 34, 35, 36 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↔ 𝑔:𝐼⟶𝐵)) |
38 | 37 | biimpa 501 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑔:𝐼⟶𝐵) |
39 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) → 𝑥 ∈ 𝐼) |
40 | 38, 39 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) → (𝑔‘𝑥) ∈ 𝐵) |
41 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) |
42 | 40, 41 | fmptd 6385 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)):(𝐵 ↑𝑚 𝐼)⟶𝐵) |
43 | | simpl2 1065 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing) |
44 | 5, 6, 11 | pwselbasb 16148 |
. . . . . . . 8
⊢ ((𝑆 ∈ CRing ∧ (𝐵 ↑𝑚
𝐼) ∈ V) → ((𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) ∈ (Base‘𝑇) ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)):(𝐵 ↑𝑚 𝐼)⟶𝐵)) |
45 | 43, 17, 44 | sylancl 694 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → ((𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) ∈ (Base‘𝑇) ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)):(𝐵 ↑𝑚 𝐼)⟶𝐵)) |
46 | 42, 45 | mpbird 247 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) ∧ 𝑥 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑥)) ∈ (Base‘𝑇)) |
47 | 46, 9 | fmptd 6385 |
. . . . 5
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑌:𝐼⟶(Base‘𝑇)) |
48 | 2, 11, 7, 3, 13, 15, 19, 32, 47 | evlseu 19516 |
. . . 4
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ∃!𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)) |
49 | | riotacl2 6624 |
. . . 4
⊢
(∃!𝑚 ∈
(𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌) → (℩𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)) ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)}) |
50 | 48, 49 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (℩𝑚 ∈ (𝑊 RingHom 𝑇)((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)) ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)}) |
51 | 10, 50 | eqeltrd 2701 |
. 2
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)}) |
52 | | coeq1 5279 |
. . . . 5
⊢ (𝑚 = 𝑄 → (𝑚 ∘ 𝐴) = (𝑄 ∘ 𝐴)) |
53 | 52 | eqeq1d 2624 |
. . . 4
⊢ (𝑚 = 𝑄 → ((𝑚 ∘ 𝐴) = 𝑋 ↔ (𝑄 ∘ 𝐴) = 𝑋)) |
54 | | coeq1 5279 |
. . . . 5
⊢ (𝑚 = 𝑄 → (𝑚 ∘ 𝑉) = (𝑄 ∘ 𝑉)) |
55 | 54 | eqeq1d 2624 |
. . . 4
⊢ (𝑚 = 𝑄 → ((𝑚 ∘ 𝑉) = 𝑌 ↔ (𝑄 ∘ 𝑉) = 𝑌)) |
56 | 53, 55 | anbi12d 747 |
. . 3
⊢ (𝑚 = 𝑄 → (((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌) ↔ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌))) |
57 | 56 | elrab 3363 |
. 2
⊢ (𝑄 ∈ {𝑚 ∈ (𝑊 RingHom 𝑇) ∣ ((𝑚 ∘ 𝐴) = 𝑋 ∧ (𝑚 ∘ 𝑉) = 𝑌)} ↔ (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌))) |
58 | 51, 57 | sylib 208 |
1
⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑄 ∈ (𝑊 RingHom 𝑇) ∧ ((𝑄 ∘ 𝐴) = 𝑋 ∧ (𝑄 ∘ 𝑉) = 𝑌))) |