Step |
Hyp |
Ref |
Expression |
1 |
|
evlsval3.q |
⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) |
2 |
|
evlsval3.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑈 ) |
3 |
|
evlsval3.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
4 |
|
evlsval3.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
5 |
|
evlsval3.k |
⊢ 𝐾 = ( Base ‘ 𝑆 ) |
6 |
|
evlsval3.u |
⊢ 𝑈 = ( 𝑆 ↾s 𝑅 ) |
7 |
|
evlsval3.t |
⊢ 𝑇 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) |
8 |
|
evlsval3.m |
⊢ 𝑀 = ( mulGrp ‘ 𝑇 ) |
9 |
|
evlsval3.w |
⊢ ↑ = ( .g ‘ 𝑀 ) |
10 |
|
evlsval3.x |
⊢ · = ( .r ‘ 𝑇 ) |
11 |
|
evlsval3.e |
⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) |
12 |
|
evlsval3.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) |
13 |
|
evlsval3.g |
⊢ 𝐺 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) |
14 |
|
evlsval3.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
15 |
|
evlsval3.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
16 |
|
evlsval3.r |
⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) |
17 |
|
eqid |
⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar 𝑈 ) |
18 |
|
eqid |
⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 ) |
19 |
1 2 17 6 7 5 18 12 13
|
evlsval |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) ) |
20 |
14 15 16 19
|
syl3anc |
⊢ ( 𝜑 → 𝑄 = ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) ) |
21 |
|
eqid |
⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 ) |
22 |
6
|
subrgcrng |
⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing ) |
23 |
15 16 22
|
syl2anc |
⊢ ( 𝜑 → 𝑈 ∈ CRing ) |
24 |
|
ovexd |
⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V ) |
25 |
7
|
pwscrng |
⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → 𝑇 ∈ CRing ) |
26 |
15 24 25
|
syl2anc |
⊢ ( 𝜑 → 𝑇 ∈ CRing ) |
27 |
5
|
subrgss |
⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 ) |
28 |
16 27
|
syl |
⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 ) |
29 |
28
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ) |
30 |
12 29
|
eqtr4id |
⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ) |
31 |
15
|
crngringd |
⊢ ( 𝜑 → 𝑆 ∈ Ring ) |
32 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) |
33 |
7 5 32
|
pwsdiagrhm |
⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) ) |
34 |
31 24 33
|
syl2anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) ) |
35 |
6
|
resrhm |
⊢ ( ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ∈ ( 𝑈 RingHom 𝑇 ) ) |
36 |
34 16 35
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ∈ ( 𝑈 RingHom 𝑇 ) ) |
37 |
30 36
|
eqeltrd |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 RingHom 𝑇 ) ) |
38 |
5
|
fvexi |
⊢ 𝐾 ∈ V |
39 |
|
elmapg |
⊢ ( ( 𝐾 ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↔ 𝑎 : 𝐼 ⟶ 𝐾 ) ) |
40 |
38 14 39
|
sylancr |
⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↔ 𝑎 : 𝐼 ⟶ 𝐾 ) ) |
41 |
40
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 ) |
42 |
41
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 ) |
43 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑥 ∈ 𝐼 ) |
44 |
42 43
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐾 ) |
45 |
44
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 ) |
46 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V ) |
47 |
7 5 21
|
pwselbasb |
⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 ) ) |
48 |
15 46 47
|
syl2an2r |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 ) ) |
49 |
45 48
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ) |
50 |
49 13
|
fmptd |
⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ ( Base ‘ 𝑇 ) ) |
51 |
2 3 21 4 8 9 10 17 11 14 23 26 37 50 18
|
evlslem1 |
⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝑃 RingHom 𝑇 ) ∧ ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) |
52 |
51
|
simp2d |
⊢ ( 𝜑 → ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ) |
53 |
51
|
simp3d |
⊢ ( 𝜑 → ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) |
54 |
51
|
simp1d |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝑃 RingHom 𝑇 ) ) |
55 |
2 21 18 17 14 23 26 37 50
|
evlseu |
⊢ ( 𝜑 → ∃! 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) |
56 |
|
coeq1 |
⊢ ( 𝑓 = 𝐸 → ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) ) |
57 |
56
|
eqeq1d |
⊢ ( 𝑓 = 𝐸 → ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ↔ ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ) ) |
58 |
|
coeq1 |
⊢ ( 𝑓 = 𝐸 → ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) ) |
59 |
58
|
eqeq1d |
⊢ ( 𝑓 = 𝐸 → ( ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ↔ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) |
60 |
57 59
|
anbi12d |
⊢ ( 𝑓 = 𝐸 → ( ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ↔ ( ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) ) |
61 |
60
|
riota2 |
⊢ ( ( 𝐸 ∈ ( 𝑃 RingHom 𝑇 ) ∧ ∃! 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) → ( ( ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ↔ ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) = 𝐸 ) ) |
62 |
54 55 61
|
syl2anc |
⊢ ( 𝜑 → ( ( ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ↔ ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) = 𝐸 ) ) |
63 |
52 53 62
|
mpbi2and |
⊢ ( 𝜑 → ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) = 𝐸 ) |
64 |
20 63
|
eqtrd |
⊢ ( 𝜑 → 𝑄 = 𝐸 ) |