Step | Hyp | Ref
| Expression |
1 | | rngunsnply.s |
. . 3
⊢ (𝜑 → 𝑆 =
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
2 | 1 | eleq2d 2870 |
. 2
⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
3 | | cnring 20253 |
. . . . . . 7
⊢
ℂfld ∈ Ring |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ Ring) |
5 | | cnfldbas 20235 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ =
(Base‘ℂfld)) |
7 | | rngunsnply.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
(SubRing‘ℂfld)) |
8 | 5 | subrgss 19230 |
. . . . . . . 8
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 𝐵 ⊆ ℂ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
10 | | rngunsnply.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
11 | 10 | snssd 4655 |
. . . . . . 7
⊢ (𝜑 → {𝑋} ⊆ ℂ) |
12 | 9, 11 | unssd 4089 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆ ℂ) |
13 | | eqidd 2798 |
. . . . . 6
⊢ (𝜑 →
(RingSpan‘ℂfld) =
(RingSpan‘ℂfld)) |
14 | | eqidd 2798 |
. . . . . 6
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) =
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
15 | | eqidd 2798 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
↾s {𝑎
∣ ∃𝑝 ∈
(Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) = (ℂfld
↾s {𝑎
∣ ∃𝑝 ∈
(Poly‘𝐵)𝑎 = (𝑝‘𝑋)})) |
16 | | cnfld0 20255 |
. . . . . . . 8
⊢ 0 =
(0g‘ℂfld) |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 =
(0g‘ℂfld)) |
18 | | cnfldadd 20236 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → + =
(+g‘ℂfld)) |
20 | | plyf 24475 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (Poly‘𝐵) → 𝑝:ℂ⟶ℂ) |
21 | | ffvelrn 6721 |
. . . . . . . . . . . 12
⊢ ((𝑝:ℂ⟶ℂ ∧
𝑋 ∈ ℂ) →
(𝑝‘𝑋) ∈ ℂ) |
22 | 20, 10, 21 | syl2anr 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑝‘𝑋) ∈ ℂ) |
23 | | eleq1 2872 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑝‘𝑋) → (𝑎 ∈ ℂ ↔ (𝑝‘𝑋) ∈ ℂ)) |
24 | 22, 23 | syl5ibrcom 248 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑎 = (𝑝‘𝑋) → 𝑎 ∈ ℂ)) |
25 | 24 | rexlimdva 3249 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) → 𝑎 ∈ ℂ)) |
26 | 25 | ss2abdv 3971 |
. . . . . . . 8
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ⊆ {𝑎 ∣ 𝑎 ∈ ℂ}) |
27 | | abid2 2928 |
. . . . . . . . 9
⊢ {𝑎 ∣ 𝑎 ∈ ℂ} = ℂ |
28 | 27, 5 | eqtri 2821 |
. . . . . . . 8
⊢ {𝑎 ∣ 𝑎 ∈ ℂ} =
(Base‘ℂfld) |
29 | 26, 28 | syl6sseq 3944 |
. . . . . . 7
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ⊆
(Base‘ℂfld)) |
30 | | abid2 2928 |
. . . . . . . . 9
⊢ {𝑎 ∣ 𝑎 ∈ 𝐵} = 𝐵 |
31 | | plyconst 24483 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ⊆ ℂ ∧ 𝑎 ∈ 𝐵) → (ℂ × {𝑎}) ∈ (Poly‘𝐵)) |
32 | 9, 31 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (ℂ × {𝑎}) ∈ (Poly‘𝐵)) |
33 | 10 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑋 ∈ ℂ) |
34 | | vex 3443 |
. . . . . . . . . . . . . . 15
⊢ 𝑎 ∈ V |
35 | 34 | fvconst2 6840 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → ((ℂ
× {𝑎})‘𝑋) = 𝑎) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((ℂ × {𝑎})‘𝑋) = 𝑎) |
37 | 36 | eqcomd 2803 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 = ((ℂ × {𝑎})‘𝑋)) |
38 | | fveq1 6544 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (ℂ × {𝑎}) → (𝑝‘𝑋) = ((ℂ × {𝑎})‘𝑋)) |
39 | 38 | rspceeqv 3579 |
. . . . . . . . . . . 12
⊢
(((ℂ × {𝑎}) ∈ (Poly‘𝐵) ∧ 𝑎 = ((ℂ × {𝑎})‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)) |
40 | 32, 37, 39 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)) |
41 | 40 | ex 413 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑎 ∈ 𝐵 → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋))) |
42 | 41 | ss2abdv 3971 |
. . . . . . . . 9
⊢ (𝜑 → {𝑎 ∣ 𝑎 ∈ 𝐵} ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
43 | 30, 42 | eqsstrrid 3943 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
44 | | subrgsubg 19235 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 𝐵 ∈
(SubGrp‘ℂfld)) |
45 | 7, 44 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
(SubGrp‘ℂfld)) |
46 | 16 | subg0cl 18045 |
. . . . . . . . 9
⊢ (𝐵 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝐵) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ 𝐵) |
48 | 43, 47 | sseldd 3896 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
49 | | biid 262 |
. . . . . . . . 9
⊢ (𝜑 ↔ 𝜑) |
50 | | vex 3443 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
51 | | eqeq1 2801 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑎 = (𝑝‘𝑋) ↔ 𝑏 = (𝑝‘𝑋))) |
52 | 51 | rexbidv 3262 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑏 = (𝑝‘𝑋))) |
53 | | fveq1 6544 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑒 → (𝑝‘𝑋) = (𝑒‘𝑋)) |
54 | 53 | eqeq2d 2807 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑒 → (𝑏 = (𝑝‘𝑋) ↔ 𝑏 = (𝑒‘𝑋))) |
55 | 54 | cbvrexv 3406 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑏 = (𝑝‘𝑋) ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) |
56 | 52, 55 | syl6bb 288 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋))) |
57 | 50, 56 | elab 3608 |
. . . . . . . . 9
⊢ (𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) |
58 | | vex 3443 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
59 | | eqeq1 2801 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → (𝑎 = (𝑝‘𝑋) ↔ 𝑐 = (𝑝‘𝑋))) |
60 | 59 | rexbidv 3262 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑐 = (𝑝‘𝑋))) |
61 | | fveq1 6544 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑑 → (𝑝‘𝑋) = (𝑑‘𝑋)) |
62 | 61 | eqeq2d 2807 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑑 → (𝑐 = (𝑝‘𝑋) ↔ 𝑐 = (𝑑‘𝑋))) |
63 | 62 | cbvrexv 3406 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑐 = (𝑝‘𝑋) ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) |
64 | 60, 63 | syl6bb 288 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋))) |
65 | 58, 64 | elab 3608 |
. . . . . . . . 9
⊢ (𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) |
66 | | simplr 765 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑒 ∈ (Poly‘𝐵)) |
67 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑑 ∈ (Poly‘𝐵)) |
68 | 18 | subrgacl 19240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 + 𝑏) ∈ 𝐵) |
69 | 68 | 3expb 1113 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
70 | 7, 69 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
71 | 70 | adantlr 711 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
72 | 71 | adantlr 711 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
73 | 66, 67, 72 | plyadd 24494 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑒 ∘𝑓 + 𝑑) ∈ (Poly‘𝐵)) |
74 | | plyf 24475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 ∈ (Poly‘𝐵) → 𝑒:ℂ⟶ℂ) |
75 | 74 | ffnd 6390 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ (Poly‘𝐵) → 𝑒 Fn ℂ) |
76 | 75 | ad2antlr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑒 Fn ℂ) |
77 | | plyf 24475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 ∈ (Poly‘𝐵) → 𝑑:ℂ⟶ℂ) |
78 | 77 | ffnd 6390 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ (Poly‘𝐵) → 𝑑 Fn ℂ) |
79 | 78 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑑 Fn ℂ) |
80 | | cnex 10471 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ
∈ V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ℂ ∈ V) |
82 | 10 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑋 ∈ ℂ) |
83 | | fnfvof 7288 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 Fn ℂ ∧ 𝑑 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑋 ∈
ℂ)) → ((𝑒
∘𝑓 + 𝑑)‘𝑋) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
84 | 76, 79, 81, 82, 83 | syl22anc 835 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒 ∘𝑓 + 𝑑)‘𝑋) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
85 | 84 | eqcomd 2803 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋)) |
86 | | fveq1 6544 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑒 ∘𝑓 + 𝑑) → (𝑝‘𝑋) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋)) |
87 | 86 | rspceeqv 3579 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∘𝑓 +
𝑑) ∈ (Poly‘𝐵) ∧ ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘𝑓 + 𝑑)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋)) |
88 | 73, 85, 87 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋)) |
89 | | oveq2 7031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑‘𝑋) → ((𝑒‘𝑋) + 𝑐) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
90 | 89 | eqeq1d 2799 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑‘𝑋) → (((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋))) |
91 | 90 | rexbidv 3262 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋))) |
92 | 88, 91 | syl5ibrcom 248 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
93 | 92 | rexlimdva 3249 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
94 | | oveq1 7030 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒‘𝑋) → (𝑏 + 𝑐) = ((𝑒‘𝑋) + 𝑐)) |
95 | 94 | eqeq1d 2799 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) → ((𝑏 + 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
96 | 95 | rexbidv 3262 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
97 | 96 | imbi2d 342 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → ((∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) ↔ (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋)))) |
98 | 93, 97 | syl5ibrcom 248 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)))) |
99 | 98 | rexlimdva 3249 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)))) |
100 | 99 | 3imp 1104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) ∧ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
101 | 49, 57, 65, 100 | syl3anb 1154 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
102 | | ovex 7055 |
. . . . . . . . 9
⊢ (𝑏 + 𝑐) ∈ V |
103 | | eqeq1 2801 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 + 𝑐) → (𝑎 = (𝑝‘𝑋) ↔ (𝑏 + 𝑐) = (𝑝‘𝑋))) |
104 | 103 | rexbidv 3262 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 + 𝑐) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋))) |
105 | 102, 104 | elab 3608 |
. . . . . . . 8
⊢ ((𝑏 + 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
106 | 101, 105 | sylibr 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → (𝑏 + 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
107 | | ax-1cn 10448 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
108 | | cnfldneg 20257 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℂ → ((invg‘ℂfld)‘1) =
-1) |
109 | 107, 108 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘ℂfld)‘1) = -1) |
110 | | cnfld1 20256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 =
(1r‘ℂfld) |
111 | 110 | subrg1cl 19237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 1 ∈ 𝐵) |
112 | 7, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈ 𝐵) |
113 | | eqid 2797 |
. . . . . . . . . . . . . . . . . . 19
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
114 | 113 | subginvcl 18046 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈
(SubGrp‘ℂfld) ∧ 1 ∈ 𝐵) →
((invg‘ℂfld)‘1) ∈ 𝐵) |
115 | 45, 112, 114 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘ℂfld)‘1) ∈ 𝐵) |
116 | 109, 115 | eqeltrrd 2886 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -1 ∈ 𝐵) |
117 | | plyconst 24483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ⊆ ℂ ∧ -1 ∈
𝐵) → (ℂ ×
{-1}) ∈ (Poly‘𝐵)) |
118 | 9, 116, 117 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ × {-1})
∈ (Poly‘𝐵)) |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (ℂ × {-1}) ∈
(Poly‘𝐵)) |
120 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑒 ∈ (Poly‘𝐵)) |
121 | | cnfldmul 20237 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
122 | 121 | subrgmcl 19241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 · 𝑏) ∈ 𝐵) |
123 | 122 | 3expb 1113 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
124 | 7, 123 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
125 | 124 | adantlr 711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
126 | 119, 120,
71, 125 | plymul 24495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ((ℂ × {-1})
∘𝑓 · 𝑒) ∈ (Poly‘𝐵)) |
127 | | ffvelrn 6721 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒:ℂ⟶ℂ ∧
𝑋 ∈ ℂ) →
(𝑒‘𝑋) ∈ ℂ) |
128 | 74, 10, 127 | syl2anr 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑒‘𝑋) ∈ ℂ) |
129 | | cnfldneg 20257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒‘𝑋) ∈ ℂ →
((invg‘ℂfld)‘(𝑒‘𝑋)) = -(𝑒‘𝑋)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) →
((invg‘ℂfld)‘(𝑒‘𝑋)) = -(𝑒‘𝑋)) |
131 | | negex 10737 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
V |
132 | | fnconstg 6442 |
. . . . . . . . . . . . . . . . 17
⊢ (-1
∈ V → (ℂ × {-1}) Fn ℂ) |
133 | 131, 132 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (ℂ × {-1}) Fn
ℂ) |
134 | 75 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑒 Fn ℂ) |
135 | 80 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ℂ ∈ V) |
136 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑋 ∈ ℂ) |
137 | | fnfvof 7288 |
. . . . . . . . . . . . . . . 16
⊢
((((ℂ × {-1}) Fn ℂ ∧ 𝑒 Fn ℂ) ∧ (ℂ ∈ V ∧
𝑋 ∈ ℂ)) →
(((ℂ × {-1}) ∘𝑓 · 𝑒)‘𝑋) = (((ℂ × {-1})‘𝑋) · (𝑒‘𝑋))) |
138 | 133, 134,
135, 136, 137 | syl22anc 835 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋) = (((ℂ × {-1})‘𝑋) · (𝑒‘𝑋))) |
139 | 131 | fvconst2 6840 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ ℂ → ((ℂ
× {-1})‘𝑋) =
-1) |
140 | 136, 139 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ((ℂ ×
{-1})‘𝑋) =
-1) |
141 | 140 | oveq1d 7038 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ ×
{-1})‘𝑋) ·
(𝑒‘𝑋)) = (-1 · (𝑒‘𝑋))) |
142 | 128 | mulm1d 10946 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (-1 · (𝑒‘𝑋)) = -(𝑒‘𝑋)) |
143 | 138, 141,
142 | 3eqtrd 2837 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋) = -(𝑒‘𝑋)) |
144 | 130, 143 | eqtr4d 2836 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) →
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋)) |
145 | | fveq1 6544 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ((ℂ × {-1})
∘𝑓 · 𝑒) → (𝑝‘𝑋) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋)) |
146 | 145 | rspceeqv 3579 |
. . . . . . . . . . . . 13
⊢
((((ℂ × {-1}) ∘𝑓 · 𝑒) ∈ (Poly‘𝐵) ∧
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘𝑓 · 𝑒)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋)) |
147 | 126, 144,
146 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋)) |
148 | | fveqeq2 6554 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) →
(((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋))) |
149 | 148 | rexbidv 3262 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋))) |
150 | 147, 149 | syl5ibrcom 248 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
151 | 150 | rexlimdva 3249 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
152 | 151 | imp 407 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
153 | 57, 152 | sylan2b 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
154 | | fvex 6558 |
. . . . . . . . 9
⊢
((invg‘ℂfld)‘𝑏) ∈ V |
155 | | eqeq1 2801 |
. . . . . . . . . 10
⊢ (𝑎 =
((invg‘ℂfld)‘𝑏) → (𝑎 = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
156 | 155 | rexbidv 3262 |
. . . . . . . . 9
⊢ (𝑎 =
((invg‘ℂfld)‘𝑏) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
157 | 154, 156 | elab 3608 |
. . . . . . . 8
⊢
(((invg‘ℂfld)‘𝑏) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
158 | 153, 157 | sylibr 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) →
((invg‘ℂfld)‘𝑏) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
159 | 110 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 =
(1r‘ℂfld)) |
160 | 121 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → · =
(.r‘ℂfld)) |
161 | 43, 112 | sseldd 3896 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
162 | 125 | adantlr 711 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
163 | 66, 67, 72, 162 | plymul 24495 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑒 ∘𝑓 · 𝑑) ∈ (Poly‘𝐵)) |
164 | | fnfvof 7288 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 Fn ℂ ∧ 𝑑 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑋 ∈
ℂ)) → ((𝑒
∘𝑓 · 𝑑)‘𝑋) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
165 | 76, 79, 81, 82, 164 | syl22anc 835 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒 ∘𝑓 · 𝑑)‘𝑋) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
166 | 165 | eqcomd 2803 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋)) |
167 | | fveq1 6544 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑒 ∘𝑓 · 𝑑) → (𝑝‘𝑋) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋)) |
168 | 167 | rspceeqv 3579 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∘𝑓
· 𝑑) ∈
(Poly‘𝐵) ∧
((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘𝑓 · 𝑑)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋)) |
169 | 163, 166,
168 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋)) |
170 | | oveq2 7031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑‘𝑋) → ((𝑒‘𝑋) · 𝑐) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
171 | 170 | eqeq1d 2799 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑‘𝑋) → (((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋))) |
172 | 171 | rexbidv 3262 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋))) |
173 | 169, 172 | syl5ibrcom 248 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
174 | 173 | rexlimdva 3249 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
175 | | oveq1 7030 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒‘𝑋) → (𝑏 · 𝑐) = ((𝑒‘𝑋) · 𝑐)) |
176 | 175 | eqeq1d 2799 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) → ((𝑏 · 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
177 | 176 | rexbidv 3262 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
178 | 177 | imbi2d 342 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → ((∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) ↔ (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋)))) |
179 | 174, 178 | syl5ibrcom 248 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)))) |
180 | 179 | rexlimdva 3249 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)))) |
181 | 180 | 3imp 1104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) ∧ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
182 | 49, 57, 65, 181 | syl3anb 1154 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
183 | | ovex 7055 |
. . . . . . . . 9
⊢ (𝑏 · 𝑐) ∈ V |
184 | | eqeq1 2801 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 · 𝑐) → (𝑎 = (𝑝‘𝑋) ↔ (𝑏 · 𝑐) = (𝑝‘𝑋))) |
185 | 184 | rexbidv 3262 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 · 𝑐) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋))) |
186 | 183, 185 | elab 3608 |
. . . . . . . 8
⊢ ((𝑏 · 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
187 | 182, 186 | sylibr 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → (𝑏 · 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
188 | 15, 17, 19, 29, 48, 106, 158, 159, 160, 161, 187, 4 | issubrngd2 19655 |
. . . . . 6
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∈
(SubRing‘ℂfld)) |
189 | | plyid 24486 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ ℂ ∧ 1 ∈
𝐵) →
Xp ∈ (Poly‘𝐵)) |
190 | 9, 112, 189 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → Xp
∈ (Poly‘𝐵)) |
191 | | df-idp 24466 |
. . . . . . . . . . . 12
⊢
Xp = ( I ↾ ℂ) |
192 | 191 | fveq1i 6546 |
. . . . . . . . . . 11
⊢
(Xp‘𝑋) = (( I ↾ ℂ)‘𝑋) |
193 | | fvresi 6805 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (( I
↾ ℂ)‘𝑋) =
𝑋) |
194 | 10, 193 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (( I ↾
ℂ)‘𝑋) = 𝑋) |
195 | 192, 194 | syl5req 2846 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = (Xp‘𝑋)) |
196 | | fveq1 6544 |
. . . . . . . . . . 11
⊢ (𝑝 = Xp →
(𝑝‘𝑋) = (Xp‘𝑋)) |
197 | 196 | rspceeqv 3579 |
. . . . . . . . . 10
⊢
((Xp ∈ (Poly‘𝐵) ∧ 𝑋 = (Xp‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋)) |
198 | 190, 195,
197 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋)) |
199 | | eqeq1 2801 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑋 → (𝑎 = (𝑝‘𝑋) ↔ 𝑋 = (𝑝‘𝑋))) |
200 | 199 | rexbidv 3262 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑋 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
201 | 200 | elabg 3607 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
202 | 10, 201 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
203 | 198, 202 | mpbird 258 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
204 | 203 | snssd 4655 |
. . . . . . 7
⊢ (𝜑 → {𝑋} ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
205 | 43, 204 | unssd 4089 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
206 | 4, 6, 12, 13, 14, 188, 205 | rgspnmin 39277 |
. . . . 5
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
207 | 206 | sseld 3894 |
. . . 4
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) → 𝑉 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)})) |
208 | | fvex 6558 |
. . . . . . 7
⊢ (𝑝‘𝑋) ∈ V |
209 | | eleq1 2872 |
. . . . . . 7
⊢ (𝑉 = (𝑝‘𝑋) → (𝑉 ∈ V ↔ (𝑝‘𝑋) ∈ V)) |
210 | 208, 209 | mpbiri 259 |
. . . . . 6
⊢ (𝑉 = (𝑝‘𝑋) → 𝑉 ∈ V) |
211 | 210 | rexlimivw 3247 |
. . . . 5
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑉 = (𝑝‘𝑋) → 𝑉 ∈ V) |
212 | | eqeq1 2801 |
. . . . . 6
⊢ (𝑎 = 𝑉 → (𝑎 = (𝑝‘𝑋) ↔ 𝑉 = (𝑝‘𝑋))) |
213 | 212 | rexbidv 3262 |
. . . . 5
⊢ (𝑎 = 𝑉 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
214 | 211, 213 | elab3 3615 |
. . . 4
⊢ (𝑉 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋)) |
215 | 207, 214 | syl6ib 252 |
. . 3
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) → ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
216 | 4, 6, 12, 13, 14 | rgspncl 39275 |
. . . . . . 7
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ∈
(SubRing‘ℂfld)) |
217 | 216 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ∈
(SubRing‘ℂfld)) |
218 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝑝 ∈ (Poly‘𝐵)) |
219 | 4, 6, 12, 13, 14 | rgspnssid 39276 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
220 | 219 | unssbd 4091 |
. . . . . . . 8
⊢ (𝜑 → {𝑋} ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
221 | | snidg 4510 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → 𝑋 ∈ {𝑋}) |
222 | 10, 221 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ {𝑋}) |
223 | 220, 222 | sseldd 3896 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
224 | 223 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝑋 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
225 | 219 | unssad 4090 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
226 | 225 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝐵 ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
227 | 217, 218,
224, 226 | cnsrplycl 39273 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑝‘𝑋) ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
228 | | eleq1 2872 |
. . . . 5
⊢ (𝑉 = (𝑝‘𝑋) → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ↔ (𝑝‘𝑋) ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
229 | 227, 228 | syl5ibrcom 248 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑉 = (𝑝‘𝑋) → 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
230 | 229 | rexlimdva 3249 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋) → 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
231 | 215, 230 | impbid 213 |
. 2
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
232 | 2, 231 | bitrd 280 |
1
⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |