Step | Hyp | Ref
| Expression |
1 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1𝑜
∈ On) |
3 | | evls1sca.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) |
4 | | evls1sca.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) |
5 | | eqid 2610 |
. . . . . . 7
⊢
((1𝑜 evalSub 𝑆)‘𝑅) = ((1𝑜 evalSub 𝑆)‘𝑅) |
6 | | eqid 2610 |
. . . . . . 7
⊢
(1𝑜 mPoly 𝑈) = (1𝑜 mPoly 𝑈) |
7 | | evls1sca.u |
. . . . . . 7
⊢ 𝑈 = (𝑆 ↾s 𝑅) |
8 | | eqid 2610 |
. . . . . . 7
⊢ (𝑆 ↑s
(𝐵
↑𝑚 1𝑜)) = (𝑆 ↑s (𝐵 ↑𝑚
1𝑜)) |
9 | | evls1sca.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
10 | 5, 6, 7, 8, 9 | evlsrhm 19342 |
. . . . . 6
⊢
((1𝑜 ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((1𝑜 evalSub
𝑆)‘𝑅) ∈ ((1𝑜 mPoly 𝑈) RingHom (𝑆 ↑s (𝐵 ↑𝑚
1𝑜)))) |
11 | 2, 3, 4, 10 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((1𝑜
evalSub 𝑆)‘𝑅) ∈ ((1𝑜
mPoly 𝑈) RingHom (𝑆 ↑s
(𝐵
↑𝑚 1𝑜)))) |
12 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(1𝑜 mPoly 𝑈)) = (Base‘(1𝑜
mPoly 𝑈)) |
13 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(𝑆
↑s (𝐵 ↑𝑚
1𝑜))) = (Base‘(𝑆 ↑s (𝐵 ↑𝑚
1𝑜))) |
14 | 12, 13 | rhmf 18549 |
. . . . 5
⊢
(((1𝑜 evalSub 𝑆)‘𝑅) ∈ ((1𝑜 mPoly 𝑈) RingHom (𝑆 ↑s (𝐵 ↑𝑚
1𝑜))) → ((1𝑜 evalSub 𝑆)‘𝑅):(Base‘(1𝑜 mPoly
𝑈))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
1𝑜)))) |
15 | 11, 14 | syl 17 |
. . . 4
⊢ (𝜑 → ((1𝑜
evalSub 𝑆)‘𝑅):(Base‘(1𝑜 mPoly
𝑈))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
1𝑜)))) |
16 | | evls1sca.a |
. . . . . . 7
⊢ 𝐴 = (algSc‘𝑊) |
17 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
18 | 7 | subrgring 18606 |
. . . . . . . . 9
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring) |
19 | 4, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ Ring) |
20 | | evls1sca.w |
. . . . . . . . 9
⊢ 𝑊 = (Poly1‘𝑈) |
21 | 20 | ply1ring 19439 |
. . . . . . . 8
⊢ (𝑈 ∈ Ring → 𝑊 ∈ Ring) |
22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Ring) |
23 | 20 | ply1lmod 19443 |
. . . . . . . 8
⊢ (𝑈 ∈ Ring → 𝑊 ∈ LMod) |
24 | 19, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
25 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
26 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
27 | 16, 17, 22, 24, 25, 26 | asclf 19158 |
. . . . . 6
⊢ (𝜑 → 𝐴:(Base‘(Scalar‘𝑊))⟶(Base‘𝑊)) |
28 | 9 | subrgss 18604 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐵) |
29 | 4, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ 𝐵) |
30 | 7, 9 | ressbas2 15758 |
. . . . . . . . 9
⊢ (𝑅 ⊆ 𝐵 → 𝑅 = (Base‘𝑈)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) |
32 | 20 | ply1sca 19444 |
. . . . . . . . . 10
⊢ (𝑈 ∈ Ring → 𝑈 = (Scalar‘𝑊)) |
33 | 19, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Scalar‘𝑊)) |
34 | 33 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑈) =
(Base‘(Scalar‘𝑊))) |
35 | 31, 34 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → 𝑅 = (Base‘(Scalar‘𝑊))) |
36 | | eqid 2610 |
. . . . . . . . . 10
⊢
(PwSer1‘𝑈) = (PwSer1‘𝑈) |
37 | 20, 36, 26 | ply1bas 19386 |
. . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘(1𝑜 mPoly 𝑈)) |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑊) =
(Base‘(1𝑜 mPoly 𝑈))) |
39 | 38 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(1𝑜 mPoly 𝑈)) = (Base‘𝑊)) |
40 | 35, 39 | feq23d 5953 |
. . . . . 6
⊢ (𝜑 → (𝐴:𝑅⟶(Base‘(1𝑜
mPoly 𝑈)) ↔ 𝐴:(Base‘(Scalar‘𝑊))⟶(Base‘𝑊))) |
41 | 27, 40 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐴:𝑅⟶(Base‘(1𝑜
mPoly 𝑈))) |
42 | | evls1sca.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑅) |
43 | 41, 42 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → (𝐴‘𝑋) ∈ (Base‘(1𝑜
mPoly 𝑈))) |
44 | | fvco3 6185 |
. . . 4
⊢
((((1𝑜 evalSub 𝑆)‘𝑅):(Base‘(1𝑜 mPoly
𝑈))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
1𝑜))) ∧ (𝐴‘𝑋) ∈ (Base‘(1𝑜
mPoly 𝑈))) → (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))‘(((1𝑜 evalSub
𝑆)‘𝑅)‘(𝐴‘𝑋)))) |
45 | 15, 43, 44 | syl2anc 691 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))‘(((1𝑜 evalSub
𝑆)‘𝑅)‘(𝐴‘𝑋)))) |
46 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (algSc‘𝑊)) |
47 | | eqid 2610 |
. . . . . . . . 9
⊢
(algSc‘𝑊) =
(algSc‘𝑊) |
48 | 20, 47 | ply1ascl 19449 |
. . . . . . . 8
⊢
(algSc‘𝑊) =
(algSc‘(1𝑜 mPoly 𝑈)) |
49 | 46, 48 | syl6eq 2660 |
. . . . . . 7
⊢ (𝜑 → 𝐴 = (algSc‘(1𝑜 mPoly
𝑈))) |
50 | 49 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑋) = ((algSc‘(1𝑜
mPoly 𝑈))‘𝑋)) |
51 | 50 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (((1𝑜
evalSub 𝑆)‘𝑅)‘(𝐴‘𝑋)) = (((1𝑜 evalSub 𝑆)‘𝑅)‘((algSc‘(1𝑜
mPoly 𝑈))‘𝑋))) |
52 | | eqid 2610 |
. . . . . 6
⊢
(algSc‘(1𝑜 mPoly 𝑈)) = (algSc‘(1𝑜
mPoly 𝑈)) |
53 | 5, 6, 7, 9, 52, 2,
3, 4, 42 | evlssca 19343 |
. . . . 5
⊢ (𝜑 → (((1𝑜
evalSub 𝑆)‘𝑅)‘((algSc‘(1𝑜
mPoly 𝑈))‘𝑋)) = ((𝐵 ↑𝑚
1𝑜) × {𝑋})) |
54 | 51, 53 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (((1𝑜
evalSub 𝑆)‘𝑅)‘(𝐴‘𝑋)) = ((𝐵 ↑𝑚
1𝑜) × {𝑋})) |
55 | 54 | fveq2d 6107 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))‘(((1𝑜 evalSub
𝑆)‘𝑅)‘(𝐴‘𝑋))) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))‘((𝐵 ↑𝑚
1𝑜) × {𝑋}))) |
56 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) = (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))) |
57 | | coeq1 5201 |
. . . . . 6
⊢ (𝑥 = ((𝐵 ↑𝑚
1𝑜) × {𝑋}) → (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) = (((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) |
58 | 57 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = ((𝐵 ↑𝑚
1𝑜) × {𝑋})) → (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) = (((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) |
59 | 29, 42 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
60 | | fconst6g 6007 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → ((𝐵 ↑𝑚
1𝑜) × {𝑋}):(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
61 | 59, 60 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐵 ↑𝑚
1𝑜) × {𝑋}):(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
62 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑆)
∈ V |
63 | 9, 62 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
64 | 63 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
65 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐵 ↑𝑚
1𝑜) ∈ V |
66 | 65 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ↑𝑚
1𝑜) ∈ V) |
67 | 64, 66 | elmapd 7758 |
. . . . . 6
⊢ (𝜑 → (((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↔ ((𝐵 ↑𝑚
1𝑜) × {𝑋}):(𝐵 ↑𝑚
1𝑜)⟶𝐵)) |
68 | 61, 67 | mpbird 246 |
. . . . 5
⊢ (𝜑 → ((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜))) |
69 | | snex 4835 |
. . . . . . . 8
⊢ {𝑋} ∈ V |
70 | 65, 69 | xpex 6860 |
. . . . . . 7
⊢ ((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∈ V |
71 | 70 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∈ V) |
72 | | mptexg 6389 |
. . . . . . 7
⊢ (𝐵 ∈ V → (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})) ∈
V) |
73 | 64, 72 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})) ∈
V) |
74 | | coexg 7010 |
. . . . . 6
⊢ ((((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∈ V ∧ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})) ∈ V) →
(((𝐵
↑𝑚 1𝑜) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) ∈
V) |
75 | 71, 73, 74 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) ∈
V) |
76 | 56, 58, 68, 75 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))‘((𝐵 ↑𝑚
1𝑜) × {𝑋})) = (((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) |
77 | | fconst6g 6007 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → (1𝑜 ×
{𝑦}):1𝑜⟶𝐵) |
78 | 77 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1𝑜 ×
{𝑦}):1𝑜⟶𝐵) |
79 | 63, 1 | pm3.2i 470 |
. . . . . . . 8
⊢ (𝐵 ∈ V ∧
1𝑜 ∈ On) |
80 | 79 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐵 ∈ V ∧ 1𝑜 ∈
On)) |
81 | | elmapg 7757 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧
1𝑜 ∈ On) → ((1𝑜 × {𝑦}) ∈ (𝐵 ↑𝑚
1𝑜) ↔ (1𝑜 × {𝑦}):1𝑜⟶𝐵)) |
82 | 80, 81 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1𝑜 ×
{𝑦}) ∈ (𝐵 ↑𝑚
1𝑜) ↔ (1𝑜 × {𝑦}):1𝑜⟶𝐵)) |
83 | 78, 82 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1𝑜 ×
{𝑦}) ∈ (𝐵 ↑𝑚
1𝑜)) |
84 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})) = (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) |
85 | | fconstmpt 5085 |
. . . . . 6
⊢ ((𝐵 ↑𝑚
1𝑜) × {𝑋}) = (𝑧 ∈ (𝐵 ↑𝑚
1𝑜) ↦ 𝑋) |
86 | 85 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝐵 ↑𝑚
1𝑜) × {𝑋}) = (𝑧 ∈ (𝐵 ↑𝑚
1𝑜) ↦ 𝑋)) |
87 | | eqidd 2611 |
. . . . 5
⊢ (𝑧 = (1𝑜
× {𝑦}) → 𝑋 = 𝑋) |
88 | 83, 84, 86, 87 | fmptco 6303 |
. . . 4
⊢ (𝜑 → (((𝐵 ↑𝑚
1𝑜) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
89 | 76, 88 | eqtrd 2644 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))‘((𝐵 ↑𝑚
1𝑜) × {𝑋})) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
90 | 45, 55, 89 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋)) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
91 | | elpwg 4116 |
. . . . . 6
⊢ (𝑅 ∈ (SubRing‘𝑆) → (𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵)) |
92 | 28, 91 | mpbird 246 |
. . . . 5
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ∈ 𝒫 𝐵) |
93 | 4, 92 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝒫 𝐵) |
94 | | evls1sca.q |
. . . . 5
⊢ 𝑄 = (𝑆 evalSub1 𝑅) |
95 | | eqid 2610 |
. . . . 5
⊢
(1𝑜 evalSub 𝑆) = (1𝑜 evalSub 𝑆) |
96 | 94, 95, 9 | evls1fval 19505 |
. . . 4
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑆)‘𝑅))) |
97 | 3, 93, 96 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑆)‘𝑅))) |
98 | 97 | fveq1d 6105 |
. 2
⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋))) |
99 | | fconstmpt 5085 |
. . 3
⊢ (𝐵 × {𝑋}) = (𝑦 ∈ 𝐵 ↦ 𝑋) |
100 | 99 | a1i 11 |
. 2
⊢ (𝜑 → (𝐵 × {𝑋}) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
101 | 90, 98, 100 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝐵 × {𝑋})) |