| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mpfrcl.q |
⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) |
| 2 |
|
ne0i |
⊢ ( 𝑋 ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) → ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ ) |
| 3 |
2 1
|
eleq2s |
⊢ ( 𝑋 ∈ 𝑄 → ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ ) |
| 4 |
|
rneq |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ∅ → ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ran ∅ ) |
| 5 |
|
rn0 |
⊢ ran ∅ = ∅ |
| 6 |
4 5
|
syl6eq |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ∅ → ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ∅ ) |
| 7 |
6
|
necon3i |
⊢ ( ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ ) |
| 8 |
|
fveq1 |
⊢ ( ( 𝐼 evalSub 𝑆 ) = ∅ → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ∅ ‘ 𝑅 ) ) |
| 9 |
|
0fv |
⊢ ( ∅ ‘ 𝑅 ) = ∅ |
| 10 |
8 9
|
syl6eq |
⊢ ( ( 𝐼 evalSub 𝑆 ) = ∅ → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ∅ ) |
| 11 |
10
|
necon3i |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → ( 𝐼 evalSub 𝑆 ) ≠ ∅ ) |
| 12 |
|
reldmevls |
⊢ Rel dom evalSub |
| 13 |
12
|
ovprc1 |
⊢ ( ¬ 𝐼 ∈ V → ( 𝐼 evalSub 𝑆 ) = ∅ ) |
| 14 |
13
|
necon1ai |
⊢ ( ( 𝐼 evalSub 𝑆 ) ≠ ∅ → 𝐼 ∈ V ) |
| 15 |
|
n0 |
⊢ ( ( 𝐼 evalSub 𝑆 ) ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ ( 𝐼 evalSub 𝑆 ) ) |
| 16 |
|
df-evls |
⊢ evalSub = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ) |
| 17 |
16
|
elmpocl2 |
⊢ ( 𝑎 ∈ ( 𝐼 evalSub 𝑆 ) → 𝑆 ∈ CRing ) |
| 18 |
17
|
a1d |
⊢ ( 𝑎 ∈ ( 𝐼 evalSub 𝑆 ) → ( 𝐼 ∈ V → 𝑆 ∈ CRing ) ) |
| 19 |
18
|
exlimiv |
⊢ ( ∃ 𝑎 𝑎 ∈ ( 𝐼 evalSub 𝑆 ) → ( 𝐼 ∈ V → 𝑆 ∈ CRing ) ) |
| 20 |
15 19
|
sylbi |
⊢ ( ( 𝐼 evalSub 𝑆 ) ≠ ∅ → ( 𝐼 ∈ V → 𝑆 ∈ CRing ) ) |
| 21 |
14 20
|
jcai |
⊢ ( ( 𝐼 evalSub 𝑆 ) ≠ ∅ → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) ) |
| 22 |
11 21
|
syl |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) ) |
| 23 |
|
fvex |
⊢ ( Base ‘ 𝑠 ) ∈ V |
| 24 |
|
nfcv |
⊢ Ⅎ 𝑏 ( SubRing ‘ 𝑠 ) |
| 25 |
|
nfcsb1v |
⊢ Ⅎ 𝑏 ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) |
| 26 |
24 25
|
nfmpt |
⊢ Ⅎ 𝑏 ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 27 |
|
csbeq1a |
⊢ ( 𝑏 = ( Base ‘ 𝑠 ) → ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 28 |
27
|
mpteq2dv |
⊢ ( 𝑏 = ( Base ‘ 𝑠 ) → ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ) |
| 29 |
23 26 28
|
csbief |
⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 30 |
|
fveq2 |
⊢ ( 𝑠 = 𝑆 → ( SubRing ‘ 𝑠 ) = ( SubRing ‘ 𝑆 ) ) |
| 31 |
30
|
adantl |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( SubRing ‘ 𝑠 ) = ( SubRing ‘ 𝑆 ) ) |
| 32 |
|
fveq2 |
⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) ) |
| 33 |
32
|
adantl |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) ) |
| 34 |
33
|
csbeq1d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 35 |
|
id |
⊢ ( 𝑖 = 𝐼 → 𝑖 = 𝐼 ) |
| 36 |
|
oveq1 |
⊢ ( 𝑠 = 𝑆 → ( 𝑠 ↾s 𝑟 ) = ( 𝑆 ↾s 𝑟 ) ) |
| 37 |
35 36
|
oveqan12d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) |
| 38 |
37
|
csbeq1d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 39 |
|
id |
⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 ) |
| 40 |
|
oveq2 |
⊢ ( 𝑖 = 𝐼 → ( 𝑏 ↑m 𝑖 ) = ( 𝑏 ↑m 𝐼 ) ) |
| 41 |
39 40
|
oveqan12rd |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) = ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) |
| 42 |
41
|
oveq2d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) = ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ) |
| 43 |
40
|
adantr |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑏 ↑m 𝑖 ) = ( 𝑏 ↑m 𝐼 ) ) |
| 44 |
43
|
xpeq1d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) = ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) |
| 45 |
44
|
mpteq2dv |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ) |
| 46 |
45
|
eqeq2d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ↔ ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ) ) |
| 47 |
35 36
|
oveqan12d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) |
| 48 |
47
|
coeq2d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) ) |
| 49 |
|
simpl |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → 𝑖 = 𝐼 ) |
| 50 |
43
|
mpteq1d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) |
| 51 |
49 50
|
mpteq12dv |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) |
| 52 |
48 51
|
eqeq12d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) |
| 53 |
46 52
|
anbi12d |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ↔ ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 54 |
42 53
|
riotaeqbidv |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 55 |
54
|
csbeq2dv |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 56 |
38 55
|
eqtrd |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 57 |
56
|
csbeq2dv |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 58 |
34 57
|
eqtrd |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 59 |
31 58
|
mpteq12dv |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ) |
| 60 |
29 59
|
syl5eq |
⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ) |
| 61 |
|
fvex |
⊢ ( SubRing ‘ 𝑆 ) ∈ V |
| 62 |
61
|
mptex |
⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ∈ V |
| 63 |
60 16 62
|
ovmpoa |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → ( 𝐼 evalSub 𝑆 ) = ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ) |
| 64 |
63
|
dmeqd |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → dom ( 𝐼 evalSub 𝑆 ) = dom ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ) |
| 65 |
|
eqid |
⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
| 66 |
65
|
dmmptss |
⊢ dom ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑆 ↑s ( 𝑏 ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ⊆ ( SubRing ‘ 𝑆 ) |
| 67 |
64 66
|
eqsstrdi |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → dom ( 𝐼 evalSub 𝑆 ) ⊆ ( SubRing ‘ 𝑆 ) ) |
| 68 |
67
|
ssneld |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → ( ¬ 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ¬ 𝑅 ∈ dom ( 𝐼 evalSub 𝑆 ) ) ) |
| 69 |
|
ndmfv |
⊢ ( ¬ 𝑅 ∈ dom ( 𝐼 evalSub 𝑆 ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ∅ ) |
| 70 |
68 69
|
syl6 |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → ( ¬ 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ∅ ) ) |
| 71 |
70
|
necon1ad |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ) |
| 72 |
71
|
com12 |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ) |
| 73 |
22 72
|
jcai |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ) |
| 74 |
|
df-3an |
⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ↔ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ) |
| 75 |
73 74
|
sylibr |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ≠ ∅ → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ) |
| 76 |
3 7 75
|
3syl |
⊢ ( 𝑋 ∈ 𝑄 → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ) |