| Step | Hyp | Ref
| Expression |
| 1 | | rngunsnply.s |
. . 3
⊢ (𝜑 → 𝑆 =
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 2 | 1 | eleq2d 2827 |
. 2
⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
| 3 | | cnring 21403 |
. . . . . . 7
⊢
ℂfld ∈ Ring |
| 4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ Ring) |
| 5 | | cnfldbas 21368 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
| 6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ =
(Base‘ℂfld)) |
| 7 | | rngunsnply.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
(SubRing‘ℂfld)) |
| 8 | 5 | subrgss 20572 |
. . . . . . . 8
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 𝐵 ⊆ ℂ) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
| 10 | | rngunsnply.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 11 | 10 | snssd 4809 |
. . . . . . 7
⊢ (𝜑 → {𝑋} ⊆ ℂ) |
| 12 | 9, 11 | unssd 4192 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆ ℂ) |
| 13 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 →
(RingSpan‘ℂfld) =
(RingSpan‘ℂfld)) |
| 14 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) =
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 15 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
↾s {𝑎
∣ ∃𝑝 ∈
(Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) = (ℂfld
↾s {𝑎
∣ ∃𝑝 ∈
(Poly‘𝐵)𝑎 = (𝑝‘𝑋)})) |
| 16 | | cnfld0 21405 |
. . . . . . . 8
⊢ 0 =
(0g‘ℂfld) |
| 17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 =
(0g‘ℂfld)) |
| 18 | | cnfldadd 21370 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
| 19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → + =
(+g‘ℂfld)) |
| 20 | | plyf 26237 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (Poly‘𝐵) → 𝑝:ℂ⟶ℂ) |
| 21 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝑝:ℂ⟶ℂ ∧
𝑋 ∈ ℂ) →
(𝑝‘𝑋) ∈ ℂ) |
| 22 | 20, 10, 21 | syl2anr 597 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑝‘𝑋) ∈ ℂ) |
| 23 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑝‘𝑋) → (𝑎 ∈ ℂ ↔ (𝑝‘𝑋) ∈ ℂ)) |
| 24 | 22, 23 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑎 = (𝑝‘𝑋) → 𝑎 ∈ ℂ)) |
| 25 | 24 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) → 𝑎 ∈ ℂ)) |
| 26 | 25 | ss2abdv 4066 |
. . . . . . . 8
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ⊆ {𝑎 ∣ 𝑎 ∈ ℂ}) |
| 27 | | abid2 2879 |
. . . . . . . . 9
⊢ {𝑎 ∣ 𝑎 ∈ ℂ} = ℂ |
| 28 | 27, 5 | eqtri 2765 |
. . . . . . . 8
⊢ {𝑎 ∣ 𝑎 ∈ ℂ} =
(Base‘ℂfld) |
| 29 | 26, 28 | sseqtrdi 4024 |
. . . . . . 7
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ⊆
(Base‘ℂfld)) |
| 30 | | abid2 2879 |
. . . . . . . . 9
⊢ {𝑎 ∣ 𝑎 ∈ 𝐵} = 𝐵 |
| 31 | | plyconst 26245 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ⊆ ℂ ∧ 𝑎 ∈ 𝐵) → (ℂ × {𝑎}) ∈ (Poly‘𝐵)) |
| 32 | 9, 31 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (ℂ × {𝑎}) ∈ (Poly‘𝐵)) |
| 33 | 10 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑋 ∈ ℂ) |
| 34 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑎 ∈ V |
| 35 | 34 | fvconst2 7224 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → ((ℂ
× {𝑎})‘𝑋) = 𝑎) |
| 36 | 33, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((ℂ × {𝑎})‘𝑋) = 𝑎) |
| 37 | 36 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 = ((ℂ × {𝑎})‘𝑋)) |
| 38 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (ℂ × {𝑎}) → (𝑝‘𝑋) = ((ℂ × {𝑎})‘𝑋)) |
| 39 | 38 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢
(((ℂ × {𝑎}) ∈ (Poly‘𝐵) ∧ 𝑎 = ((ℂ × {𝑎})‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)) |
| 40 | 32, 37, 39 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)) |
| 41 | 40 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑎 ∈ 𝐵 → ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋))) |
| 42 | 41 | ss2abdv 4066 |
. . . . . . . . 9
⊢ (𝜑 → {𝑎 ∣ 𝑎 ∈ 𝐵} ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 43 | 30, 42 | eqsstrrid 4023 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 44 | | subrgsubg 20577 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 𝐵 ∈
(SubGrp‘ℂfld)) |
| 45 | 7, 44 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
(SubGrp‘ℂfld)) |
| 46 | 16 | subg0cl 19152 |
. . . . . . . . 9
⊢ (𝐵 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝐵) |
| 47 | 45, 46 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ 𝐵) |
| 48 | 43, 47 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 49 | | biid 261 |
. . . . . . . . 9
⊢ (𝜑 ↔ 𝜑) |
| 50 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
| 51 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑎 = (𝑝‘𝑋) ↔ 𝑏 = (𝑝‘𝑋))) |
| 52 | 51 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑏 = (𝑝‘𝑋))) |
| 53 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑒 → (𝑝‘𝑋) = (𝑒‘𝑋)) |
| 54 | 53 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑒 → (𝑏 = (𝑝‘𝑋) ↔ 𝑏 = (𝑒‘𝑋))) |
| 55 | 54 | cbvrexvw 3238 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑏 = (𝑝‘𝑋) ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) |
| 56 | 52, 55 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋))) |
| 57 | 50, 56 | elab 3679 |
. . . . . . . . 9
⊢ (𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) |
| 58 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
| 59 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → (𝑎 = (𝑝‘𝑋) ↔ 𝑐 = (𝑝‘𝑋))) |
| 60 | 59 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑐 = (𝑝‘𝑋))) |
| 61 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑑 → (𝑝‘𝑋) = (𝑑‘𝑋)) |
| 62 | 61 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑑 → (𝑐 = (𝑝‘𝑋) ↔ 𝑐 = (𝑑‘𝑋))) |
| 63 | 62 | cbvrexvw 3238 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑐 = (𝑝‘𝑋) ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) |
| 64 | 60, 63 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋))) |
| 65 | 58, 64 | elab 3679 |
. . . . . . . . 9
⊢ (𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) |
| 66 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑒 ∈ (Poly‘𝐵)) |
| 67 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑑 ∈ (Poly‘𝐵)) |
| 68 | 18 | subrgacl 20583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 + 𝑏) ∈ 𝐵) |
| 69 | 68 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
| 70 | 7, 69 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
| 71 | 70 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
| 72 | 71 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ∈ 𝐵) |
| 73 | 66, 67, 72 | plyadd 26256 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑒 ∘f + 𝑑) ∈ (Poly‘𝐵)) |
| 74 | | plyf 26237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 ∈ (Poly‘𝐵) → 𝑒:ℂ⟶ℂ) |
| 75 | 74 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 ∈ (Poly‘𝐵) → 𝑒 Fn ℂ) |
| 76 | 75 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑒 Fn ℂ) |
| 77 | | plyf 26237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 ∈ (Poly‘𝐵) → 𝑑:ℂ⟶ℂ) |
| 78 | 77 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ (Poly‘𝐵) → 𝑑 Fn ℂ) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑑 Fn ℂ) |
| 80 | | cnex 11236 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ
∈ V |
| 81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ℂ ∈ V) |
| 82 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → 𝑋 ∈ ℂ) |
| 83 | | fnfvof 7714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 Fn ℂ ∧ 𝑑 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑋 ∈
ℂ)) → ((𝑒
∘f + 𝑑)‘𝑋) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
| 84 | 76, 79, 81, 82, 83 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒 ∘f + 𝑑)‘𝑋) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
| 85 | 84 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘f + 𝑑)‘𝑋)) |
| 86 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑒 ∘f + 𝑑) → (𝑝‘𝑋) = ((𝑒 ∘f + 𝑑)‘𝑋)) |
| 87 | 86 | rspceeqv 3645 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∘f + 𝑑) ∈ (Poly‘𝐵) ∧ ((𝑒‘𝑋) + (𝑑‘𝑋)) = ((𝑒 ∘f + 𝑑)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋)) |
| 88 | 73, 85, 87 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋)) |
| 89 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑‘𝑋) → ((𝑒‘𝑋) + 𝑐) = ((𝑒‘𝑋) + (𝑑‘𝑋))) |
| 90 | 89 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑‘𝑋) → (((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋))) |
| 91 | 90 | rexbidv 3179 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + (𝑑‘𝑋)) = (𝑝‘𝑋))) |
| 92 | 88, 91 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
| 93 | 92 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
| 94 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒‘𝑋) → (𝑏 + 𝑐) = ((𝑒‘𝑋) + 𝑐)) |
| 95 | 94 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) → ((𝑏 + 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
| 96 | 95 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋))) |
| 97 | 96 | imbi2d 340 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → ((∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) ↔ (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) + 𝑐) = (𝑝‘𝑋)))) |
| 98 | 93, 97 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)))) |
| 99 | 98 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)))) |
| 100 | 99 | 3imp 1111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) ∧ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
| 101 | 49, 57, 65, 100 | syl3anb 1162 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
| 102 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑏 + 𝑐) ∈ V |
| 103 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 + 𝑐) → (𝑎 = (𝑝‘𝑋) ↔ (𝑏 + 𝑐) = (𝑝‘𝑋))) |
| 104 | 103 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 + 𝑐) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋))) |
| 105 | 102, 104 | elab 3679 |
. . . . . . . 8
⊢ ((𝑏 + 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 + 𝑐) = (𝑝‘𝑋)) |
| 106 | 101, 105 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → (𝑏 + 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 107 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
| 108 | | cnfldneg 21408 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℂ → ((invg‘ℂfld)‘1) =
-1) |
| 109 | 107, 108 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘ℂfld)‘1) = -1) |
| 110 | | cnfld1 21406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 =
(1r‘ℂfld) |
| 111 | 110 | subrg1cl 20580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
(SubRing‘ℂfld) → 1 ∈ 𝐵) |
| 112 | 7, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈ 𝐵) |
| 113 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
| 114 | 113 | subginvcl 19153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈
(SubGrp‘ℂfld) ∧ 1 ∈ 𝐵) →
((invg‘ℂfld)‘1) ∈ 𝐵) |
| 115 | 45, 112, 114 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((invg‘ℂfld)‘1) ∈ 𝐵) |
| 116 | 109, 115 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -1 ∈ 𝐵) |
| 117 | | plyconst 26245 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ⊆ ℂ ∧ -1 ∈
𝐵) → (ℂ ×
{-1}) ∈ (Poly‘𝐵)) |
| 118 | 9, 116, 117 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ × {-1})
∈ (Poly‘𝐵)) |
| 119 | 118 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (ℂ × {-1}) ∈
(Poly‘𝐵)) |
| 120 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑒 ∈ (Poly‘𝐵)) |
| 121 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
| 122 | 121 | subrgmcl 20584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 · 𝑏) ∈ 𝐵) |
| 123 | 122 | 3expb 1121 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
(SubRing‘ℂfld) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
| 124 | 7, 123 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
| 125 | 124 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
| 126 | 119, 120,
71, 125 | plymul 26257 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ((ℂ × {-1})
∘f · 𝑒) ∈ (Poly‘𝐵)) |
| 127 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒:ℂ⟶ℂ ∧
𝑋 ∈ ℂ) →
(𝑒‘𝑋) ∈ ℂ) |
| 128 | 74, 10, 127 | syl2anr 597 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑒‘𝑋) ∈ ℂ) |
| 129 | | cnfldneg 21408 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒‘𝑋) ∈ ℂ →
((invg‘ℂfld)‘(𝑒‘𝑋)) = -(𝑒‘𝑋)) |
| 130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) →
((invg‘ℂfld)‘(𝑒‘𝑋)) = -(𝑒‘𝑋)) |
| 131 | | negex 11506 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
V |
| 132 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . 17
⊢ (-1
∈ V → (ℂ × {-1}) Fn ℂ) |
| 133 | 131, 132 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (ℂ × {-1}) Fn
ℂ) |
| 134 | 75 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑒 Fn ℂ) |
| 135 | 80 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ℂ ∈ V) |
| 136 | 10 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → 𝑋 ∈ ℂ) |
| 137 | | fnfvof 7714 |
. . . . . . . . . . . . . . . 16
⊢
((((ℂ × {-1}) Fn ℂ ∧ 𝑒 Fn ℂ) ∧ (ℂ ∈ V ∧
𝑋 ∈ ℂ)) →
(((ℂ × {-1}) ∘f · 𝑒)‘𝑋) = (((ℂ × {-1})‘𝑋) · (𝑒‘𝑋))) |
| 138 | 133, 134,
135, 136, 137 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ × {-1})
∘f · 𝑒)‘𝑋) = (((ℂ × {-1})‘𝑋) · (𝑒‘𝑋))) |
| 139 | 131 | fvconst2 7224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ ℂ → ((ℂ
× {-1})‘𝑋) =
-1) |
| 140 | 136, 139 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ((ℂ ×
{-1})‘𝑋) =
-1) |
| 141 | 140 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ ×
{-1})‘𝑋) ·
(𝑒‘𝑋)) = (-1 · (𝑒‘𝑋))) |
| 142 | 128 | mulm1d 11715 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (-1 · (𝑒‘𝑋)) = -(𝑒‘𝑋)) |
| 143 | 138, 141,
142 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (((ℂ × {-1})
∘f · 𝑒)‘𝑋) = -(𝑒‘𝑋)) |
| 144 | 130, 143 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) →
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘f · 𝑒)‘𝑋)) |
| 145 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ((ℂ × {-1})
∘f · 𝑒) → (𝑝‘𝑋) = (((ℂ × {-1})
∘f · 𝑒)‘𝑋)) |
| 146 | 145 | rspceeqv 3645 |
. . . . . . . . . . . . 13
⊢
((((ℂ × {-1}) ∘f · 𝑒) ∈ (Poly‘𝐵) ∧
((invg‘ℂfld)‘(𝑒‘𝑋)) = (((ℂ × {-1})
∘f · 𝑒)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋)) |
| 147 | 126, 144,
146 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋)) |
| 148 | | fveqeq2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) →
(((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋))) |
| 149 | 148 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘(𝑒‘𝑋)) = (𝑝‘𝑋))) |
| 150 | 147, 149 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
| 151 | 150 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
| 152 | 151 | imp 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
| 153 | 57, 152 | sylan2b 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
| 154 | | fvex 6919 |
. . . . . . . . 9
⊢
((invg‘ℂfld)‘𝑏) ∈ V |
| 155 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑎 =
((invg‘ℂfld)‘𝑏) → (𝑎 = (𝑝‘𝑋) ↔
((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
| 156 | 155 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑎 =
((invg‘ℂfld)‘𝑏) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋))) |
| 157 | 154, 156 | elab 3679 |
. . . . . . . 8
⊢
(((invg‘ℂfld)‘𝑏) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)((invg‘ℂfld)‘𝑏) = (𝑝‘𝑋)) |
| 158 | 153, 157 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) →
((invg‘ℂfld)‘𝑏) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 159 | 110 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 =
(1r‘ℂfld)) |
| 160 | 121 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → · =
(.r‘ℂfld)) |
| 161 | 43, 112 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 162 | 125 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
| 163 | 66, 67, 72, 162 | plymul 26257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑒 ∘f · 𝑑) ∈ (Poly‘𝐵)) |
| 164 | | fnfvof 7714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 Fn ℂ ∧ 𝑑 Fn ℂ) ∧ (ℂ
∈ V ∧ 𝑋 ∈
ℂ)) → ((𝑒
∘f · 𝑑)‘𝑋) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
| 165 | 76, 79, 81, 82, 164 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒 ∘f · 𝑑)‘𝑋) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
| 166 | 165 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘f · 𝑑)‘𝑋)) |
| 167 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑒 ∘f · 𝑑) → (𝑝‘𝑋) = ((𝑒 ∘f · 𝑑)‘𝑋)) |
| 168 | 167 | rspceeqv 3645 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∘f ·
𝑑) ∈ (Poly‘𝐵) ∧ ((𝑒‘𝑋) · (𝑑‘𝑋)) = ((𝑒 ∘f · 𝑑)‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋)) |
| 169 | 163, 166,
168 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋)) |
| 170 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑‘𝑋) → ((𝑒‘𝑋) · 𝑐) = ((𝑒‘𝑋) · (𝑑‘𝑋))) |
| 171 | 170 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑‘𝑋) → (((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋))) |
| 172 | 171 | rexbidv 3179 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · (𝑑‘𝑋)) = (𝑝‘𝑋))) |
| 173 | 169, 172 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) ∧ 𝑑 ∈ (Poly‘𝐵)) → (𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
| 174 | 173 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
| 175 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒‘𝑋) → (𝑏 · 𝑐) = ((𝑒‘𝑋) · 𝑐)) |
| 176 | 175 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒‘𝑋) → ((𝑏 · 𝑐) = (𝑝‘𝑋) ↔ ((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
| 177 | 176 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑋) → (∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋))) |
| 178 | 177 | imbi2d 340 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑋) → ((∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) ↔ (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)((𝑒‘𝑋) · 𝑐) = (𝑝‘𝑋)))) |
| 179 | 174, 178 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ∈ (Poly‘𝐵)) → (𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)))) |
| 180 | 179 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) → (∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)))) |
| 181 | 180 | 3imp 1111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑒 ∈ (Poly‘𝐵)𝑏 = (𝑒‘𝑋) ∧ ∃𝑑 ∈ (Poly‘𝐵)𝑐 = (𝑑‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
| 182 | 49, 57, 65, 181 | syl3anb 1162 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
| 183 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑏 · 𝑐) ∈ V |
| 184 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑏 · 𝑐) → (𝑎 = (𝑝‘𝑋) ↔ (𝑏 · 𝑐) = (𝑝‘𝑋))) |
| 185 | 184 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑎 = (𝑏 · 𝑐) → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋))) |
| 186 | 183, 185 | elab 3679 |
. . . . . . . 8
⊢ ((𝑏 · 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)(𝑏 · 𝑐) = (𝑝‘𝑋)) |
| 187 | 182, 186 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∧ 𝑐 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) → (𝑏 · 𝑐) ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 188 | 15, 17, 19, 29, 48, 106, 158, 159, 160, 161, 187, 4 | issubrgd 21196 |
. . . . . 6
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ∈
(SubRing‘ℂfld)) |
| 189 | | plyid 26248 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ ℂ ∧ 1 ∈
𝐵) →
Xp ∈ (Poly‘𝐵)) |
| 190 | 9, 112, 189 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → Xp
∈ (Poly‘𝐵)) |
| 191 | | df-idp 26228 |
. . . . . . . . . . . 12
⊢
Xp = ( I ↾ ℂ) |
| 192 | 191 | fveq1i 6907 |
. . . . . . . . . . 11
⊢
(Xp‘𝑋) = (( I ↾ ℂ)‘𝑋) |
| 193 | | fvresi 7193 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (( I
↾ ℂ)‘𝑋) =
𝑋) |
| 194 | 10, 193 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (( I ↾
ℂ)‘𝑋) = 𝑋) |
| 195 | 192, 194 | eqtr2id 2790 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = (Xp‘𝑋)) |
| 196 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑝 = Xp →
(𝑝‘𝑋) = (Xp‘𝑋)) |
| 197 | 196 | rspceeqv 3645 |
. . . . . . . . . 10
⊢
((Xp ∈ (Poly‘𝐵) ∧ 𝑋 = (Xp‘𝑋)) → ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋)) |
| 198 | 190, 195,
197 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋)) |
| 199 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑋 → (𝑎 = (𝑝‘𝑋) ↔ 𝑋 = (𝑝‘𝑋))) |
| 200 | 199 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑎 = 𝑋 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑋 = (𝑝‘𝑋))) |
| 201 | 10, 198, 200 | elabd 3681 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 202 | 201 | snssd 4809 |
. . . . . . 7
⊢ (𝜑 → {𝑋} ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 203 | 43, 202 | unssd 4192 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 204 | 4, 6, 12, 13, 14, 188, 203 | rgspnmin 20615 |
. . . . 5
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ⊆ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)}) |
| 205 | 204 | sseld 3982 |
. . . 4
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) → 𝑉 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)})) |
| 206 | | fvex 6919 |
. . . . . . 7
⊢ (𝑝‘𝑋) ∈ V |
| 207 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑉 = (𝑝‘𝑋) → (𝑉 ∈ V ↔ (𝑝‘𝑋) ∈ V)) |
| 208 | 206, 207 | mpbiri 258 |
. . . . . 6
⊢ (𝑉 = (𝑝‘𝑋) → 𝑉 ∈ V) |
| 209 | 208 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑝 ∈
(Poly‘𝐵)𝑉 = (𝑝‘𝑋) → 𝑉 ∈ V) |
| 210 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑎 = 𝑉 → (𝑎 = (𝑝‘𝑋) ↔ 𝑉 = (𝑝‘𝑋))) |
| 211 | 210 | rexbidv 3179 |
. . . . 5
⊢ (𝑎 = 𝑉 → (∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
| 212 | 209, 211 | elab3 3686 |
. . . 4
⊢ (𝑉 ∈ {𝑎 ∣ ∃𝑝 ∈ (Poly‘𝐵)𝑎 = (𝑝‘𝑋)} ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋)) |
| 213 | 205, 212 | imbitrdi 251 |
. . 3
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) → ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
| 214 | 4, 6, 12, 13, 14 | rgspncl 20613 |
. . . . . . 7
⊢ (𝜑 →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ∈
(SubRing‘ℂfld)) |
| 215 | 214 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) →
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ∈
(SubRing‘ℂfld)) |
| 216 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝑝 ∈ (Poly‘𝐵)) |
| 217 | 4, 6, 12, 13, 14 | rgspnssid 20614 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∪ {𝑋}) ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 218 | 217 | unssbd 4194 |
. . . . . . . 8
⊢ (𝜑 → {𝑋} ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 219 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → 𝑋 ∈ {𝑋}) |
| 220 | 10, 219 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ {𝑋}) |
| 221 | 218, 220 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 222 | 221 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝑋 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 223 | 217 | unssad 4193 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 224 | 223 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → 𝐵 ⊆
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 225 | 215, 216,
222, 224 | cnsrplycl 43179 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑝‘𝑋) ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋}))) |
| 226 | | eleq1 2829 |
. . . . 5
⊢ (𝑉 = (𝑝‘𝑋) → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ↔ (𝑝‘𝑋) ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
| 227 | 225, 226 | syl5ibrcom 247 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (Poly‘𝐵)) → (𝑉 = (𝑝‘𝑋) → 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
| 228 | 227 | rexlimdva 3155 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋) → 𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))) |
| 229 | 213, 228 | impbid 212 |
. 2
⊢ (𝜑 → (𝑉 ∈
((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})) ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |
| 230 | 2, 229 | bitrd 279 |
1
⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋))) |