Step | Hyp | Ref
| Expression |
1 | | 1on 7833 |
. . . . . . 7
⊢
1o ∈ On |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1o ∈
On) |
3 | | evls1sca.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) |
4 | | evls1sca.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) |
5 | | eqid 2825 |
. . . . . . 7
⊢
((1o evalSub 𝑆)‘𝑅) = ((1o evalSub 𝑆)‘𝑅) |
6 | | eqid 2825 |
. . . . . . 7
⊢
(1o mPoly 𝑈) = (1o mPoly 𝑈) |
7 | | evls1sca.u |
. . . . . . 7
⊢ 𝑈 = (𝑆 ↾s 𝑅) |
8 | | eqid 2825 |
. . . . . . 7
⊢ (𝑆 ↑s
(𝐵
↑𝑚 1o)) = (𝑆 ↑s (𝐵 ↑𝑚
1o)) |
9 | | evls1sca.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
10 | 5, 6, 7, 8, 9 | evlsrhm 19881 |
. . . . . 6
⊢
((1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((1o evalSub 𝑆)‘𝑅) ∈ ((1o mPoly 𝑈) RingHom (𝑆 ↑s (𝐵 ↑𝑚
1o)))) |
11 | 2, 3, 4, 10 | syl3anc 1496 |
. . . . 5
⊢ (𝜑 → ((1o evalSub
𝑆)‘𝑅) ∈ ((1o mPoly 𝑈) RingHom (𝑆 ↑s (𝐵 ↑𝑚
1o)))) |
12 | | eqid 2825 |
. . . . . 6
⊢
(Base‘(1o mPoly 𝑈)) = (Base‘(1o mPoly 𝑈)) |
13 | | eqid 2825 |
. . . . . 6
⊢
(Base‘(𝑆
↑s (𝐵 ↑𝑚 1o)))
= (Base‘(𝑆
↑s (𝐵 ↑𝑚
1o))) |
14 | 12, 13 | rhmf 19082 |
. . . . 5
⊢
(((1o evalSub 𝑆)‘𝑅) ∈ ((1o mPoly 𝑈) RingHom (𝑆 ↑s (𝐵 ↑𝑚
1o))) → ((1o evalSub 𝑆)‘𝑅):(Base‘(1o mPoly 𝑈))⟶(Base‘(𝑆 ↑s
(𝐵
↑𝑚 1o)))) |
15 | 11, 14 | syl 17 |
. . . 4
⊢ (𝜑 → ((1o evalSub
𝑆)‘𝑅):(Base‘(1o mPoly 𝑈))⟶(Base‘(𝑆 ↑s
(𝐵
↑𝑚 1o)))) |
16 | | evls1sca.a |
. . . . . . 7
⊢ 𝐴 = (algSc‘𝑊) |
17 | | eqid 2825 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
18 | 7 | subrgring 19139 |
. . . . . . . . 9
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring) |
19 | 4, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ Ring) |
20 | | evls1sca.w |
. . . . . . . . 9
⊢ 𝑊 = (Poly1‘𝑈) |
21 | 20 | ply1ring 19978 |
. . . . . . . 8
⊢ (𝑈 ∈ Ring → 𝑊 ∈ Ring) |
22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Ring) |
23 | 20 | ply1lmod 19982 |
. . . . . . . 8
⊢ (𝑈 ∈ Ring → 𝑊 ∈ LMod) |
24 | 19, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
25 | | eqid 2825 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
26 | | eqid 2825 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
27 | 16, 17, 22, 24, 25, 26 | asclf 19698 |
. . . . . 6
⊢ (𝜑 → 𝐴:(Base‘(Scalar‘𝑊))⟶(Base‘𝑊)) |
28 | 9 | subrgss 19137 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐵) |
29 | 4, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ 𝐵) |
30 | 7, 9 | ressbas2 16294 |
. . . . . . . . 9
⊢ (𝑅 ⊆ 𝐵 → 𝑅 = (Base‘𝑈)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) |
32 | 20 | ply1sca 19983 |
. . . . . . . . . 10
⊢ (𝑈 ∈ Ring → 𝑈 = (Scalar‘𝑊)) |
33 | 19, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Scalar‘𝑊)) |
34 | 33 | fveq2d 6437 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑈) =
(Base‘(Scalar‘𝑊))) |
35 | 31, 34 | eqtrd 2861 |
. . . . . . 7
⊢ (𝜑 → 𝑅 = (Base‘(Scalar‘𝑊))) |
36 | | eqid 2825 |
. . . . . . . . . 10
⊢
(PwSer1‘𝑈) = (PwSer1‘𝑈) |
37 | 20, 36, 26 | ply1bas 19925 |
. . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘(1o mPoly 𝑈)) |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑊) = (Base‘(1o
mPoly 𝑈))) |
39 | 38 | eqcomd 2831 |
. . . . . . 7
⊢ (𝜑 → (Base‘(1o
mPoly 𝑈)) =
(Base‘𝑊)) |
40 | 35, 39 | feq23d 6273 |
. . . . . 6
⊢ (𝜑 → (𝐴:𝑅⟶(Base‘(1o mPoly
𝑈)) ↔ 𝐴:(Base‘(Scalar‘𝑊))⟶(Base‘𝑊))) |
41 | 27, 40 | mpbird 249 |
. . . . 5
⊢ (𝜑 → 𝐴:𝑅⟶(Base‘(1o mPoly
𝑈))) |
42 | | evls1sca.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑅) |
43 | 41, 42 | ffvelrnd 6609 |
. . . 4
⊢ (𝜑 → (𝐴‘𝑋) ∈ (Base‘(1o mPoly
𝑈))) |
44 | | fvco3 6522 |
. . . 4
⊢
((((1o evalSub 𝑆)‘𝑅):(Base‘(1o mPoly 𝑈))⟶(Base‘(𝑆 ↑s
(𝐵
↑𝑚 1o))) ∧ (𝐴‘𝑋) ∈ (Base‘(1o mPoly
𝑈))) → (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) ∘
((1o evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))‘(((1o evalSub 𝑆)‘𝑅)‘(𝐴‘𝑋)))) |
45 | 15, 43, 44 | syl2anc 581 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) ∘
((1o evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))‘(((1o evalSub 𝑆)‘𝑅)‘(𝐴‘𝑋)))) |
46 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (algSc‘𝑊)) |
47 | | eqid 2825 |
. . . . . . . . 9
⊢
(algSc‘𝑊) =
(algSc‘𝑊) |
48 | 20, 47 | ply1ascl 19988 |
. . . . . . . 8
⊢
(algSc‘𝑊) =
(algSc‘(1o mPoly 𝑈)) |
49 | 46, 48 | syl6eq 2877 |
. . . . . . 7
⊢ (𝜑 → 𝐴 = (algSc‘(1o mPoly 𝑈))) |
50 | 49 | fveq1d 6435 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑋) = ((algSc‘(1o mPoly 𝑈))‘𝑋)) |
51 | 50 | fveq2d 6437 |
. . . . 5
⊢ (𝜑 → (((1o evalSub
𝑆)‘𝑅)‘(𝐴‘𝑋)) = (((1o evalSub 𝑆)‘𝑅)‘((algSc‘(1o mPoly
𝑈))‘𝑋))) |
52 | | eqid 2825 |
. . . . . 6
⊢
(algSc‘(1o mPoly 𝑈)) = (algSc‘(1o mPoly 𝑈)) |
53 | 5, 6, 7, 9, 52, 2,
3, 4, 42 | evlssca 19882 |
. . . . 5
⊢ (𝜑 → (((1o evalSub
𝑆)‘𝑅)‘((algSc‘(1o mPoly
𝑈))‘𝑋)) = ((𝐵 ↑𝑚 1o)
× {𝑋})) |
54 | 51, 53 | eqtrd 2861 |
. . . 4
⊢ (𝜑 → (((1o evalSub
𝑆)‘𝑅)‘(𝐴‘𝑋)) = ((𝐵 ↑𝑚 1o)
× {𝑋})) |
55 | 54 | fveq2d 6437 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))‘(((1o evalSub 𝑆)‘𝑅)‘(𝐴‘𝑋))) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))‘((𝐵 ↑𝑚
1o) × {𝑋}))) |
56 | | eqidd 2826 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) = (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))) |
57 | | coeq1 5512 |
. . . . . 6
⊢ (𝑥 = ((𝐵 ↑𝑚 1o)
× {𝑋}) → (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) = (((𝐵 ↑𝑚 1o)
× {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) |
58 | 57 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = ((𝐵 ↑𝑚 1o)
× {𝑋})) → (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) = (((𝐵 ↑𝑚 1o)
× {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) |
59 | 29, 42 | sseldd 3828 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
60 | | fconst6g 6331 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → ((𝐵 ↑𝑚 1o)
× {𝑋}):(𝐵 ↑𝑚
1o)⟶𝐵) |
61 | 59, 60 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐵 ↑𝑚 1o)
× {𝑋}):(𝐵 ↑𝑚
1o)⟶𝐵) |
62 | 9 | fvexi 6447 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
64 | | ovex 6937 |
. . . . . . . 8
⊢ (𝐵 ↑𝑚
1o) ∈ V |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ↑𝑚 1o)
∈ V) |
66 | 63, 65 | elmapd 8136 |
. . . . . 6
⊢ (𝜑 → (((𝐵 ↑𝑚 1o)
× {𝑋}) ∈ (𝐵 ↑𝑚
(𝐵
↑𝑚 1o)) ↔ ((𝐵 ↑𝑚 1o)
× {𝑋}):(𝐵 ↑𝑚
1o)⟶𝐵)) |
67 | 61, 66 | mpbird 249 |
. . . . 5
⊢ (𝜑 → ((𝐵 ↑𝑚 1o)
× {𝑋}) ∈ (𝐵 ↑𝑚
(𝐵
↑𝑚 1o))) |
68 | | snex 5129 |
. . . . . . . 8
⊢ {𝑋} ∈ V |
69 | 64, 68 | xpex 7223 |
. . . . . . 7
⊢ ((𝐵 ↑𝑚
1o) × {𝑋})
∈ V |
70 | 69 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((𝐵 ↑𝑚 1o)
× {𝑋}) ∈
V) |
71 | | mptexg 6740 |
. . . . . . 7
⊢ (𝐵 ∈ V → (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})) ∈ V) |
72 | 63, 71 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})) ∈ V) |
73 | | coexg 7379 |
. . . . . 6
⊢ ((((𝐵 ↑𝑚
1o) × {𝑋})
∈ V ∧ (𝑦 ∈
𝐵 ↦ (1o
× {𝑦})) ∈ V)
→ (((𝐵
↑𝑚 1o) × {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ V) |
74 | 70, 72, 73 | syl2anc 581 |
. . . . 5
⊢ (𝜑 → (((𝐵 ↑𝑚 1o)
× {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) ∈ V) |
75 | 56, 58, 67, 74 | fvmptd 6535 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))‘((𝐵 ↑𝑚
1o) × {𝑋})) = (((𝐵 ↑𝑚 1o)
× {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) |
76 | | fconst6g 6331 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → (1o × {𝑦}):1o⟶𝐵) |
77 | 76 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1o × {𝑦}):1o⟶𝐵) |
78 | 62, 1 | pm3.2i 464 |
. . . . . . . 8
⊢ (𝐵 ∈ V ∧ 1o
∈ On) |
79 | 78 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐵 ∈ V ∧ 1o ∈
On)) |
80 | | elmapg 8135 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ 1o
∈ On) → ((1o × {𝑦}) ∈ (𝐵 ↑𝑚 1o)
↔ (1o × {𝑦}):1o⟶𝐵)) |
81 | 79, 80 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1o × {𝑦}) ∈ (𝐵 ↑𝑚 1o)
↔ (1o × {𝑦}):1o⟶𝐵)) |
82 | 77, 81 | mpbird 249 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1o × {𝑦}) ∈ (𝐵 ↑𝑚
1o)) |
83 | | eqidd 2826 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})) = (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) |
84 | | fconstmpt 5398 |
. . . . . 6
⊢ ((𝐵 ↑𝑚
1o) × {𝑋})
= (𝑧 ∈ (𝐵 ↑𝑚
1o) ↦ 𝑋) |
85 | 84 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝐵 ↑𝑚 1o)
× {𝑋}) = (𝑧 ∈ (𝐵 ↑𝑚 1o)
↦ 𝑋)) |
86 | | eqidd 2826 |
. . . . 5
⊢ (𝑧 = (1o × {𝑦}) → 𝑋 = 𝑋) |
87 | 82, 83, 85, 86 | fmptco 6646 |
. . . 4
⊢ (𝜑 → (((𝐵 ↑𝑚 1o)
× {𝑋}) ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
88 | 75, 87 | eqtrd 2861 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦}))))‘((𝐵 ↑𝑚
1o) × {𝑋})) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
89 | 45, 55, 88 | 3eqtrd 2865 |
. 2
⊢ (𝜑 → (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) ∘
((1o evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋)) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
90 | | elpwg 4386 |
. . . . . 6
⊢ (𝑅 ∈ (SubRing‘𝑆) → (𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵)) |
91 | 28, 90 | mpbird 249 |
. . . . 5
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ∈ 𝒫 𝐵) |
92 | 4, 91 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝒫 𝐵) |
93 | | evls1sca.q |
. . . . 5
⊢ 𝑄 = (𝑆 evalSub1 𝑅) |
94 | | eqid 2825 |
. . . . 5
⊢
(1o evalSub 𝑆) = (1o evalSub 𝑆) |
95 | 93, 94, 9 | evls1fval 20044 |
. . . 4
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) ∘
((1o evalSub 𝑆)‘𝑅))) |
96 | 3, 92, 95 | syl2anc 581 |
. . 3
⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) ∘
((1o evalSub 𝑆)‘𝑅))) |
97 | 96 | fveq1d 6435 |
. 2
⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1o)) ↦ (𝑥
∘ (𝑦 ∈ 𝐵 ↦ (1o ×
{𝑦})))) ∘
((1o evalSub 𝑆)‘𝑅))‘(𝐴‘𝑋))) |
98 | | fconstmpt 5398 |
. . 3
⊢ (𝐵 × {𝑋}) = (𝑦 ∈ 𝐵 ↦ 𝑋) |
99 | 98 | a1i 11 |
. 2
⊢ (𝜑 → (𝐵 × {𝑋}) = (𝑦 ∈ 𝐵 ↦ 𝑋)) |
100 | 89, 97, 99 | 3eqtr4d 2871 |
1
⊢ (𝜑 → (𝑄‘(𝐴‘𝑋)) = (𝐵 × {𝑋})) |