Step | Hyp | Ref
| Expression |
1 | | algnbval.2 |
. . 3
⊢ (𝜑 → 𝐸 ∈ Field) |
2 | 1 | elexd 3463 |
. 2
⊢ (𝜑 → 𝐸 ∈ V) |
3 | | algnbval.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
4 | 3 | elexd 3463 |
. 2
⊢ (𝜑 → 𝐹 ∈ V) |
5 | | algnbval.o |
. . . . . . 7
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
6 | 5 | ovexi 7385 |
. . . . . 6
⊢ 𝑂 ∈ V |
7 | 6 | dmex 7840 |
. . . . 5
⊢ dom 𝑂 ∈ V |
8 | 7 | difexi 5283 |
. . . 4
⊢ (dom
𝑂 ∖ {𝑍}) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → (dom 𝑂 ∖ {𝑍}) ∈ V) |
10 | | fvex 6852 |
. . . . . 6
⊢ (𝑂‘𝑝) ∈ V |
11 | 10 | cnvex 7854 |
. . . . 5
⊢ ◡(𝑂‘𝑝) ∈ V |
12 | 11 | imaex 7845 |
. . . 4
⊢ (◡(𝑂‘𝑝) “ { 0 }) ∈
V |
13 | 12 | rgenw 3066 |
. . 3
⊢
∀𝑝 ∈
(dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ∈
V |
14 | | iunexg 7888 |
. . 3
⊢ (((dom
𝑂 ∖ {𝑍}) ∈ V ∧ ∀𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ∈ V) →
∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ∈
V) |
15 | 9, 13, 14 | sylancl 586 |
. 2
⊢ (𝜑 → ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ∈
V) |
16 | | oveq12 7360 |
. . . . . . 7
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝑒 evalSub1 𝑓) = (𝐸 evalSub1 𝐹)) |
17 | 16, 5 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝑒 evalSub1 𝑓) = 𝑂) |
18 | 17 | dmeqd 5859 |
. . . . 5
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → dom (𝑒 evalSub1 𝑓) = dom 𝑂) |
19 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → 𝑒 = 𝐸) |
20 | 19 | fveq2d 6843 |
. . . . . . . 8
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (Poly1‘𝑒) =
(Poly1‘𝐸)) |
21 | 20 | fveq2d 6843 |
. . . . . . 7
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) →
(0g‘(Poly1‘𝑒)) =
(0g‘(Poly1‘𝐸))) |
22 | | algnbval.z |
. . . . . . 7
⊢ 𝑍 =
(0g‘(Poly1‘𝐸)) |
23 | 21, 22 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) →
(0g‘(Poly1‘𝑒)) = 𝑍) |
24 | 23 | sneqd 4596 |
. . . . 5
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) →
{(0g‘(Poly1‘𝑒))} = {𝑍}) |
25 | 18, 24 | difeq12d 4081 |
. . . 4
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (dom (𝑒 evalSub1 𝑓) ∖
{(0g‘(Poly1‘𝑒))}) = (dom 𝑂 ∖ {𝑍})) |
26 | 17 | fveq1d 6841 |
. . . . . 6
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → ((𝑒 evalSub1 𝑓)‘𝑝) = (𝑂‘𝑝)) |
27 | 26 | cnveqd 5829 |
. . . . 5
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → ◡((𝑒 evalSub1 𝑓)‘𝑝) = ◡(𝑂‘𝑝)) |
28 | 19 | fveq2d 6843 |
. . . . . . 7
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (0g‘𝑒) = (0g‘𝐸)) |
29 | | algnbval.1 |
. . . . . . 7
⊢ 0 =
(0g‘𝐸) |
30 | 28, 29 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (0g‘𝑒) = 0 ) |
31 | 30 | sneqd 4596 |
. . . . 5
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → {(0g‘𝑒)} = { 0 }) |
32 | 27, 31 | imaeq12d 6012 |
. . . 4
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (◡((𝑒 evalSub1 𝑓)‘𝑝) “ {(0g‘𝑒)}) = (◡(𝑂‘𝑝) “ { 0 })) |
33 | 25, 32 | iuneq12d 4980 |
. . 3
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → ∪
𝑝 ∈ (dom (𝑒 evalSub1 𝑓) ∖
{(0g‘(Poly1‘𝑒))})(◡((𝑒 evalSub1 𝑓)‘𝑝) “ {(0g‘𝑒)}) = ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |
34 | | df-algnb 32172 |
. . 3
⊢ AlgNb =
(𝑒 ∈ V, 𝑓 ∈ V ↦ ∪ 𝑝 ∈ (dom (𝑒 evalSub1 𝑓) ∖
{(0g‘(Poly1‘𝑒))})(◡((𝑒 evalSub1 𝑓)‘𝑝) “ {(0g‘𝑒)})) |
35 | 33, 34 | ovmpoga 7503 |
. 2
⊢ ((𝐸 ∈ V ∧ 𝐹 ∈ V ∧ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ∈ V) → (𝐸 AlgNb 𝐹) = ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |
36 | 2, 4, 15, 35 | syl3anc 1371 |
1
⊢ (𝜑 → (𝐸 AlgNb 𝐹) = ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |