Step | Hyp | Ref
| Expression |
1 | | rngunsnply.s |
. . 3
⊢ (𝜑 → 𝑆 =
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
2 | 1 | eleq2d 2673 |
. 2
⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
3 | | cnring 19587 |
. . . . . . 7
⊢
ℂfld ∈ Ring |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ Ring) |
5 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ =
(Base‘ℂfld)) |
7 | | rngunsnply.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
(SubRing‘ℂfld)) |
8 | 5 | subrgss 18604 |
. . . . . . . 8
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 𝐵 ⊆ ℂ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
10 | | rngunsnply.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
11 | 10 | snssd 4281 |
. . . . . . 7
⊢ (𝜑 → {𝑋} ⊆ ℂ) |
12 | 9, 11 | unssd 3751 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆ ℂ) |
13 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 →
(RingSpan‘ℂfld) =
(RingSpan‘ℂfld)) |
14 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) =
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
15 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
↾s {𝑎
∣ ∃𝑝 ∈
(Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) = (ℂfld
↾s {𝑎
∣ ∃𝑝 ∈
(Poly‘𝐵)𝑎 = (𝑝‘𝑋)})) |
16 | | cnfld0 19589 |
. . . . . . . 8
⊢ 0 =
(0g‘ℂfld) |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 =
(0g‘ℂfld)) |
18 | | cnfldadd 19572 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → + =
(+g‘ℂfld)) |
20 | | plyf 23758 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (Poly‘𝐵) → 𝑝:ℂ⟶ℂ) |
21 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑝:ℂ⟶ℂ ∧
𝑋 ∈ ℂ) →
(𝑝‘𝑋) ∈ ℂ) |
22 | 20, 10, 21 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑝‘𝑋) ∈ ℂ) |
23 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑝‘𝑋) → (𝑎 ∈ ℂ ↔ (𝑝‘𝑋) ∈ ℂ)) |
24 | 22, 23 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑎 = (𝑝‘𝑋) → 𝑎 ∈ ℂ)) |
25 | 24 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) → 𝑎 ∈ ℂ)) |
26 | 25 | ss2abdv 3638 |
. . . . . . . 8
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ⊆ {𝑎 ∣ 𝑎 ∈ ℂ}) |
27 | | abid2 2732 |
. . . . . . . . 9
⊢ {𝑎 ∣ 𝑎 ∈ ℂ} = ℂ |
28 | 27, 5 | eqtri 2632 |
. . . . . . . 8
⊢ {𝑎 ∣ 𝑎 ∈ ℂ} =
(Base‘ℂfld) |
29 | 26, 28 | syl6sseq 3614 |
. . . . . . 7
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ⊆
(Base‘ℂfld)) |
30 | | abid2 2732 |
. . . . . . . . 9
⊢ {𝑎 ∣ 𝑎 ∈ 𝐵} = 𝐵 |
31 | | plyconst 23766 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ⊆ ℂ ∧ 𝑎 ∈ 𝐵) → (ℂ × {𝑎}) ∈ (Poly‘𝐵)) |
32 | 9, 31 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (ℂ × {𝑎}) ∈ (Poly‘𝐵)) |
33 | 10 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑋 ∈ ℂ) |
34 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑎 ∈ V |
35 | 34 | fvconst2 6374 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → ((ℂ
× {𝑎})‘𝑋) = 𝑎) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((ℂ × {𝑎})‘𝑋) = 𝑎) |
37 | 36 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 = ((ℂ × {𝑎})‘𝑋)) |
38 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = (ℂ × {𝑎}) → (𝑝‘𝑋) = ((ℂ × {𝑎})‘𝑋)) |
39 | 38 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (ℂ × {𝑎}) → (𝑎 = (𝑝‘𝑋) ↔ 𝑎 = ((ℂ × {𝑎})‘𝑋))) |
40 | 39 | rspcev 3282 |
. . . . . . . . . . . 12
⊢
(((ℂ × {𝑎}) ∈ (Poly‘𝐵) ∧ 𝑎 = ((ℂ × {𝑎})‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)) |
41 | 32, 37, 40 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)) |
42 | 41 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑎 ∈ 𝐵 → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋))) |
43 | 42 | ss2abdv 3638 |
. . . . . . . . 9
⊢ (𝜑 → {𝑎 ∣ 𝑎 ∈ 𝐵} ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
44 | 30, 43 | syl5eqssr 3613 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
45 | | subrgsubg 18609 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 𝐵 ∈
(SubGrp‘ℂfld)) |
46 | 7, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
(SubGrp‘ℂfld)) |
47 | 16 | subg0cl 17425 |
. . . . . . . . 9
⊢ (𝐵 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝐵) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ 𝐵) |
49 | 44, 48 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
50 | | biid 250 |
. . . . . . . . 9
⊢ (𝜑 ↔ 𝜑) |
51 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
52 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑎 = (𝑝‘𝑋) ↔ 𝑏 = (𝑝‘𝑋))) |
53 | 52 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑏 = (𝑝‘𝑋))) |
54 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑒 → (𝑝‘𝑋) = (𝑒‘𝑋)) |
55 | 54 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑒 → (𝑏 = (𝑝‘𝑋) ↔ 𝑏 = (𝑒‘𝑋))) |
56 | 55 | cbvrexv 3148 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑏 = (𝑝‘𝑋) ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) |
57 | 53, 56 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋))) |
58 | 51, 57 | elab 3319 |
. . . . . . . . 9
⊢ (𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) |
59 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
60 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → (𝑎 = (𝑝‘𝑋) ↔ 𝑐 = (𝑝‘𝑋))) |
61 | 60 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑐 = (𝑝‘𝑋))) |
62 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑑 → (𝑝‘𝑋) = (𝑑‘𝑋)) |
63 | 62 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑑 → (𝑐 = (𝑝‘𝑋) ↔ 𝑐 = (𝑑‘𝑋))) |
64 | 63 | cbvrexv 3148 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑐 = (𝑝‘𝑋) ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) |
65 | 61, 64 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋))) |
66 | 59, 65 | elab 3319 |
. . . . . . . . 9
⊢ (𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) |
67 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑒 ∈ (Poly‘𝐵)) |
68 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑑 ∈ (Poly‘𝐵)) |
69 | 18 | subrgacl 18614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 + 𝑏) ∈ 𝐵) |
70 | 69 | 3expb 1258 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
71 | 7, 70 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
72 | 71 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
73 | 72 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
74 | 67, 68, 73 | plyadd 23777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑒 ∘𝑓 + 𝑑) ∈ (Poly‘𝐵)) |
75 | | plyf 23758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 ∈ (Poly‘𝐵) → 𝑒:ℂ⟶ℂ) |
76 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒:ℂ⟶ℂ →
𝑒 Fn
ℂ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ (Poly‘𝐵) → 𝑒 Fn ℂ) |
78 | 77 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑒 Fn ℂ) |
79 | | plyf 23758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 ∈ (Poly‘𝐵) → 𝑑:ℂ⟶ℂ) |
80 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑:ℂ⟶ℂ →
𝑑 Fn
ℂ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ (Poly‘𝐵) → 𝑑 Fn ℂ) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑑 Fn ℂ) |
83 | | cnex 9896 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ
∈ V |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ℂ ∈ V) |
85 | 10 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑋 ∈ ℂ) |
86 | | fnfvof 6809 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 Fn ℂ ∧ 𝑑 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑋 ∈
ℂ)) → ((𝑒
∘𝑓 + 𝑑)‘𝑋) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
87 | 78, 82, 84, 85, 86 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒 ∘𝑓 + 𝑑)‘𝑋) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
88 | 87 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋)) |
89 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = (𝑒 ∘𝑓 + 𝑑) → (𝑝‘𝑋) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋)) |
90 | 89 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑒 ∘𝑓 + 𝑑) → (((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋))) |
91 | 90 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∘𝑓 +
𝑑) ∈ (Poly‘𝐵) ∧ ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋)) |
92 | 74, 88, 91 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋)) |
93 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑‘𝑋) → ((𝑒‘𝑋) + 𝑐) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
94 | 93 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑‘𝑋) → (((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋))) |
95 | 94 | rexbidv 3034 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋))) |
96 | 92, 95 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
97 | 96 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
98 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒‘𝑋) → (𝑏 + 𝑐) = ((𝑒‘𝑋) + 𝑐)) |
99 | 98 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) → ((𝑏 + 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
100 | 99 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
101 | 100 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → ((∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) ↔ (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋)))) |
102 | 97, 101 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)))) |
103 | 102 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)))) |
104 | 103 | 3imp 1249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) ∧ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
105 | 50, 58, 66, 104 | syl3anb 1361 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
106 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑏 + 𝑐) ∈ V |
107 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 + 𝑐) → (𝑎 = (𝑝‘𝑋) ↔ (𝑏 + 𝑐) = (𝑝‘𝑋))) |
108 | 107 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 + 𝑐) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋))) |
109 | 106, 108 | elab 3319 |
. . . . . . . 8
⊢ ((𝑏 + 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
110 | 105, 109 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → (𝑏 + 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
111 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
112 | | cnfldneg 19591 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℂ → ((invg‘ℂfld)‘1) =
-1) |
113 | 111, 112 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘ℂfld)‘1) = -1) |
114 | | cnfld1 19590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 =
(1r‘ℂfld) |
115 | 114 | subrg1cl 18611 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 1 ∈ 𝐵) |
116 | 7, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈ 𝐵) |
117 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
118 | 117 | subginvcl 17426 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈
(SubGrp‘ℂfld) ∧ 1 ∈ 𝐵) →
((invg‘ℂfld)‘1) ∈ 𝐵) |
119 | 46, 116, 118 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘ℂfld)‘1) ∈ 𝐵) |
120 | 113, 119 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -1 ∈ 𝐵) |
121 | | plyconst 23766 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ⊆ ℂ ∧ -1 ∈
𝐵) → (ℂ ×
{-1}) ∈ (Poly‘𝐵)) |
122 | 9, 120, 121 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ × {-1})
∈ (Poly‘𝐵)) |
123 | 122 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (ℂ × {-1}) ∈
(Poly‘𝐵)) |
124 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑒 ∈ (Poly‘𝐵)) |
125 | | cnfldmul 19573 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
126 | 125 | subrgmcl 18615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 · 𝑏) ∈ 𝐵) |
127 | 126 | 3expb 1258 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
128 | 7, 127 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
129 | 128 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
130 | 123, 124,
72, 129 | plymul 23778 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ((ℂ × {-1})
∘𝑓 · 𝑒) ∈ (Poly‘𝐵)) |
131 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒:ℂ⟶ℂ ∧
𝑋 ∈ ℂ) →
(𝑒‘𝑋) ∈ ℂ) |
132 | 75, 10, 131 | syl2anr 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑒‘𝑋) ∈ ℂ) |
133 | | cnfldneg 19591 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒‘𝑋) ∈ ℂ →
((invg‘ℂfld)‘(𝑒‘𝑋)) = -(𝑒‘𝑋)) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) →
((invg‘ℂfld)‘(𝑒‘𝑋)) = -(𝑒‘𝑋)) |
135 | | negex 10158 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
V |
136 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . 17
⊢ (-1
∈ V → (ℂ × {-1}) Fn ℂ) |
137 | 135, 136 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (ℂ × {-1}) Fn
ℂ) |
138 | 77 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑒 Fn ℂ) |
139 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ℂ ∈ V) |
140 | 10 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑋 ∈ ℂ) |
141 | | fnfvof 6809 |
. . . . . . . . . . . . . . . 16
⊢
((((ℂ × {-1}) Fn ℂ ∧ 𝑒 Fn ℂ) ∧ (ℂ ∈ V ∧
𝑋 ∈ ℂ)) →
(((ℂ × {-1}) ∘𝑓 · 𝑒)‘𝑋) = (((ℂ × {-1})‘𝑋) · (𝑒‘𝑋))) |
142 | 137, 138,
139, 140, 141 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋) = (((ℂ × {-1})‘𝑋) · (𝑒‘𝑋))) |
143 | 135 | fvconst2 6374 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ ℂ → ((ℂ
× {-1})‘𝑋) =
-1) |
144 | 140, 143 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ((ℂ ×
{-1})‘𝑋) =
-1) |
145 | 144 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ ×
{-1})‘𝑋) ·
(𝑒‘𝑋)) = (-1 · (𝑒‘𝑋))) |
146 | 132 | mulm1d 10361 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (-1 · (𝑒‘𝑋)) = -(𝑒‘𝑋)) |
147 | 142, 145,
146 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋) = -(𝑒‘𝑋)) |
148 | 134, 147 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) →
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋)) |
149 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = ((ℂ × {-1})
∘𝑓 · 𝑒) → (𝑝‘𝑋) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋)) |
150 | 149 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ((ℂ × {-1})
∘𝑓 · 𝑒) →
(((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋))) |
151 | 150 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢
((((ℂ × {-1}) ∘𝑓 · 𝑒) ∈ (Poly‘𝐵) ∧
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋)) |
152 | 130, 148,
151 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋)) |
153 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) →
((invg‘ℂfld)‘𝑏) =
((invg‘ℂfld)‘(𝑒‘𝑋))) |
154 | 153 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) →
(((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋))) |
155 | 154 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋))) |
156 | 152, 155 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
157 | 156 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
158 | 157 | imp 444 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
159 | 58, 158 | sylan2b 491 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
160 | | fvex 6113 |
. . . . . . . . 9
⊢
((invg‘ℂfld)‘𝑏) ∈ V |
161 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑎 =
((invg‘ℂfld)‘𝑏) → (𝑎 = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
162 | 161 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑎 =
((invg‘ℂfld)‘𝑏) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
163 | 160, 162 | elab 3319 |
. . . . . . . 8
⊢
(((invg‘ℂfld)‘𝑏) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
164 | 159, 163 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) →
((invg‘ℂfld)‘𝑏) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
165 | 114 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 =
(1r‘ℂfld)) |
166 | 125 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → · =
(.r‘ℂfld)) |
167 | 44, 116 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
168 | 129 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
169 | 67, 68, 73, 168 | plymul 23778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑒 ∘𝑓 · 𝑑) ∈ (Poly‘𝐵)) |
170 | | fnfvof 6809 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 Fn ℂ ∧ 𝑑 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑋 ∈
ℂ)) → ((𝑒
∘𝑓 · 𝑑)‘𝑋) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
171 | 78, 82, 84, 85, 170 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒 ∘𝑓 · 𝑑)‘𝑋) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
172 | 171 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋)) |
173 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = (𝑒 ∘𝑓 · 𝑑) → (𝑝‘𝑋) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋)) |
174 | 173 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑒 ∘𝑓 · 𝑑) → (((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋))) |
175 | 174 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∘𝑓
· 𝑑) ∈
(Poly‘𝐵) ∧
((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋)) |
176 | 169, 172,
175 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋)) |
177 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑‘𝑋) → ((𝑒‘𝑋) · 𝑐) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
178 | 177 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑‘𝑋) → (((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋))) |
179 | 178 | rexbidv 3034 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋))) |
180 | 176, 179 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
181 | 180 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
182 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒‘𝑋) → (𝑏 · 𝑐) = ((𝑒‘𝑋) · 𝑐)) |
183 | 182 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) → ((𝑏 · 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
184 | 183 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
185 | 184 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → ((∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) ↔ (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋)))) |
186 | 181, 185 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)))) |
187 | 186 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)))) |
188 | 187 | 3imp 1249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) ∧ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
189 | 50, 58, 66, 188 | syl3anb 1361 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
190 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑏 · 𝑐) ∈ V |
191 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 · 𝑐) → (𝑎 = (𝑝‘𝑋) ↔ (𝑏 · 𝑐) = (𝑝‘𝑋))) |
192 | 191 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 · 𝑐) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋))) |
193 | 190, 192 | elab 3319 |
. . . . . . . 8
⊢ ((𝑏 · 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
194 | 189, 193 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → (𝑏 · 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
195 | 15, 17, 19, 29, 49, 110, 164, 165, 166, 167, 194, 4 | issubrngd2 19010 |
. . . . . 6
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∈
(SubRing‘ℂfld)) |
196 | | plyid 23769 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ ℂ ∧ 1 ∈
𝐵) →
Xp ∈ (Poly‘𝐵)) |
197 | 9, 116, 196 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → Xp
∈ (Poly‘𝐵)) |
198 | | df-idp 23749 |
. . . . . . . . . . . 12
⊢
Xp = ( I ↾ ℂ) |
199 | 198 | fveq1i 6104 |
. . . . . . . . . . 11
⊢
(Xp‘𝑋) = (( I ↾ ℂ)‘𝑋) |
200 | | fvresi 6344 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (( I
↾ ℂ)‘𝑋) =
𝑋) |
201 | 10, 200 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (( I ↾
ℂ)‘𝑋) = 𝑋) |
202 | 199, 201 | syl5req 2657 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = (Xp‘𝑋)) |
203 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑝 = Xp →
(𝑝‘𝑋) = (Xp‘𝑋)) |
204 | 203 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑝 = Xp →
(𝑋 = (𝑝‘𝑋) ↔ 𝑋 = (Xp‘𝑋))) |
205 | 204 | rspcev 3282 |
. . . . . . . . . 10
⊢
((Xp ∈ (Poly‘𝐵) ∧ 𝑋 = (Xp‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋)) |
206 | 197, 202,
205 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋)) |
207 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑋 → (𝑎 = (𝑝‘𝑋) ↔ 𝑋 = (𝑝‘𝑋))) |
208 | 207 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑋 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
209 | 208 | elabg 3320 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
210 | 10, 209 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
211 | 206, 210 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
212 | 211 | snssd 4281 |
. . . . . . 7
⊢ (𝜑 → {𝑋} ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
213 | 44, 212 | unssd 3751 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
214 | 4, 6, 12, 13, 14, 195, 213 | rgspnmin 36760 |
. . . . 5
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
215 | 214 | sseld 3567 |
. . . 4
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) → 𝑉 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)})) |
216 | | fvex 6113 |
. . . . . . 7
⊢ (𝑝‘𝑋) ∈ V |
217 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑉 = (𝑝‘𝑋) → (𝑉 ∈ V ↔ (𝑝‘𝑋) ∈ V)) |
218 | 216, 217 | mpbiri 247 |
. . . . . 6
⊢ (𝑉 = (𝑝‘𝑋) → 𝑉 ∈ V) |
219 | 218 | rexlimivw 3011 |
. . . . 5
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑉 = (𝑝‘𝑋) → 𝑉 ∈ V) |
220 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑎 = 𝑉 → (𝑎 = (𝑝‘𝑋) ↔ 𝑉 = (𝑝‘𝑋))) |
221 | 220 | rexbidv 3034 |
. . . . 5
⊢ (𝑎 = 𝑉 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
222 | 219, 221 | elab3 3327 |
. . . 4
⊢ (𝑉 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋)) |
223 | 215, 222 | syl6ib 240 |
. . 3
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) → ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
224 | 4, 6, 12, 13, 14 | rgspncl 36758 |
. . . . . . 7
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ∈
(SubRing‘ℂfld)) |
225 | 224 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ∈
(SubRing‘ℂfld)) |
226 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝑝 ∈ (Poly‘𝐵)) |
227 | 4, 6, 12, 13, 14 | rgspnssid 36759 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
228 | 227 | unssbd 3753 |
. . . . . . . 8
⊢ (𝜑 → {𝑋} ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
229 | | snidg 4153 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → 𝑋 ∈ {𝑋}) |
230 | 10, 229 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ {𝑋}) |
231 | 228, 230 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
232 | 231 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝑋 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
233 | 227 | unssad 3752 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
234 | 233 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝐵 ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
235 | 225, 226,
232, 234 | cnsrplycl 36756 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑝‘𝑋) ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
236 | | eleq1 2676 |
. . . . 5
⊢ (𝑉 = (𝑝‘𝑋) → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ↔ (𝑝‘𝑋) ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
237 | 235, 236 | syl5ibrcom 236 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑉 = (𝑝‘𝑋) → 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
238 | 237 | rexlimdva 3013 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋) → 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
239 | 223, 238 | impbid 201 |
. 2
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
240 | 2, 239 | bitrd 267 |
1
⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |