Metamath Proof Explorer

Theorem rngunsnply

Description: Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Hypotheses rngunsnply.b ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ ℂfld ) )
rngunsnply.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
rngunsnply.s ⊢ ( 𝜑 → 𝑆 = ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
Assertion rngunsnply ( 𝜑 → ( 𝑉 ∈ 𝑆 ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 rngunsnply.b ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ ℂfld ) )
2 rngunsnply.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3 rngunsnply.s ⊢ ( 𝜑 → 𝑆 = ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
4 3 eleq2d ⊢ ( 𝜑 → ( 𝑉 ∈ 𝑆 ↔ 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ) )
5 cnring ⊢ ℂfld ∈ Ring
6 5 a1i ⊢ ( 𝜑 → ℂfld ∈ Ring )
7 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
8 7 a1i ⊢ ( 𝜑 → ℂ = ( Base ‘ ℂfld ) )
9 7 subrgss ⊢ ( 𝐵 ∈ ( SubRing ‘ ℂfld ) → 𝐵 ⊆ ℂ )
10 1 9 syl ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
11 2 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ ℂ )
12 10 11 unssd ⊢ ( 𝜑 → ( 𝐵 ∪ { 𝑋 } ) ⊆ ℂ )
13 eqidd ⊢ ( 𝜑 → ( RingSpan ‘ ℂfld ) = ( RingSpan ‘ ℂfld ) )
14 eqidd ⊢ ( 𝜑 → ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) = ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
15 eqidd ⊢ ( 𝜑 → ( ℂfld ↾s { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) = ( ℂfld ↾s { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) )
16 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
17 16 a1i ⊢ ( 𝜑 → 0 = ( 0g ‘ ℂfld ) )
18 cnfldadd ⊢ + = ( +g ‘ ℂfld )
19 18 a1i ⊢ ( 𝜑 → + = ( +g ‘ ℂfld ) )
20 plyf ⊢ ( 𝑝 ∈ ( Poly ‘ 𝐵 ) → 𝑝 : ℂ ⟶ ℂ )
21 ffvelrn ⊢ ( ( 𝑝 : ℂ ⟶ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑝 ‘ 𝑋 ) ∈ ℂ )
22 20 2 21 syl2anr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑝 ‘ 𝑋 ) ∈ ℂ )
23 eleq1 ⊢ ( 𝑎 = ( 𝑝 ‘ 𝑋 ) → ( 𝑎 ∈ ℂ ↔ ( 𝑝 ‘ 𝑋 ) ∈ ℂ ) )
24 22 23 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) → 𝑎 ∈ ℂ ) )
25 24 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) → 𝑎 ∈ ℂ ) )
26 25 ss2abdv ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ⊆ { 𝑎 ∣ 𝑎 ∈ ℂ } )
27 abid2 ⊢ { 𝑎 ∣ 𝑎 ∈ ℂ } = ℂ
28 27 7 eqtri ⊢ { 𝑎 ∣ 𝑎 ∈ ℂ } = ( Base ‘ ℂfld )
29 26 28 sseqtrdi ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ⊆ ( Base ‘ ℂfld ) )
30 abid2 ⊢ { 𝑎 ∣ 𝑎 ∈ 𝐵 } = 𝐵
31 plyconst ⊢ ( ( 𝐵 ⊆ ℂ ∧ 𝑎 ∈ 𝐵 ) → ( ℂ × { 𝑎 } ) ∈ ( Poly ‘ 𝐵 ) )
32 10 31 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ℂ × { 𝑎 } ) ∈ ( Poly ‘ 𝐵 ) )
33 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ ℂ )
34 vex ⊢ 𝑎 ∈ V
35 34 fvconst2 ⊢ ( 𝑋 ∈ ℂ → ( ( ℂ × { 𝑎 } ) ‘ 𝑋 ) = 𝑎 )
36 33 35 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ℂ × { 𝑎 } ) ‘ 𝑋 ) = 𝑎 )
37 36 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 = ( ( ℂ × { 𝑎 } ) ‘ 𝑋 ) )
38 fveq1 ⊢ ( 𝑝 = ( ℂ × { 𝑎 } ) → ( 𝑝 ‘ 𝑋 ) = ( ( ℂ × { 𝑎 } ) ‘ 𝑋 ) )
39 38 rspceeqv ⊢ ( ( ( ℂ × { 𝑎 } ) ∈ ( Poly ‘ 𝐵 ) ∧ 𝑎 = ( ( ℂ × { 𝑎 } ) ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) )
40 32 37 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) )
41 40 ex ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ) )
42 41 ss2abdv ⊢ ( 𝜑 → { 𝑎 ∣ 𝑎 ∈ 𝐵 } ⊆ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
43 30 42 eqsstrrid ⊢ ( 𝜑 → 𝐵 ⊆ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
44 subrgsubg ⊢ ( 𝐵 ∈ ( SubRing ‘ ℂfld ) → 𝐵 ∈ ( SubGrp ‘ ℂfld ) )
45 1 44 syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ ℂfld ) )
46 16 subg0cl ⊢ ( 𝐵 ∈ ( SubGrp ‘ ℂfld ) → 0 ∈ 𝐵 )
47 45 46 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
48 43 47 sseldd ⊢ ( 𝜑 → 0 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
49 biid ⊢ ( 𝜑 ↔ 𝜑 )
50 vex ⊢ 𝑏 ∈ V
51 eqeq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ 𝑏 = ( 𝑝 ‘ 𝑋 ) ) )
52 51 rexbidv ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑝 ‘ 𝑋 ) ) )
53 fveq1 ⊢ ( 𝑝 = 𝑒 → ( 𝑝 ‘ 𝑋 ) = ( 𝑒 ‘ 𝑋 ) )
54 53 eqeq2d ⊢ ( 𝑝 = 𝑒 → ( 𝑏 = ( 𝑝 ‘ 𝑋 ) ↔ 𝑏 = ( 𝑒 ‘ 𝑋 ) ) )
55 54 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) )
56 52 55 bitrdi ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) ) )
57 50 56 elab ⊢ ( 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ↔ ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) )
58 vex ⊢ 𝑐 ∈ V
59 eqeq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ 𝑐 = ( 𝑝 ‘ 𝑋 ) ) )
60 59 rexbidv ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑝 ‘ 𝑋 ) ) )
61 fveq1 ⊢ ( 𝑝 = 𝑑 → ( 𝑝 ‘ 𝑋 ) = ( 𝑑 ‘ 𝑋 ) )
62 61 eqeq2d ⊢ ( 𝑝 = 𝑑 → ( 𝑐 = ( 𝑝 ‘ 𝑋 ) ↔ 𝑐 = ( 𝑑 ‘ 𝑋 ) ) )
63 62 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) )
64 60 63 bitrdi ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) ) )
65 58 64 elab ⊢ ( 𝑐 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ↔ ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) )
66 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → 𝑒 ∈ ( Poly ‘ 𝐵 ) )
67 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → 𝑑 ∈ ( Poly ‘ 𝐵 ) )
68 18 subrgacl ⊢ ( ( 𝐵 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
69 68 3expb ⊢ ( ( 𝐵 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
70 1 69 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
71 70 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
72 71 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
73 66 67 72 plyadd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑒 ∘f + 𝑑 ) ∈ ( Poly ‘ 𝐵 ) )
74 plyf ⊢ ( 𝑒 ∈ ( Poly ‘ 𝐵 ) → 𝑒 : ℂ ⟶ ℂ )
75 74 ffnd ⊢ ( 𝑒 ∈ ( Poly ‘ 𝐵 ) → 𝑒 Fn ℂ )
76 75 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → 𝑒 Fn ℂ )
77 plyf ⊢ ( 𝑑 ∈ ( Poly ‘ 𝐵 ) → 𝑑 : ℂ ⟶ ℂ )
78 77 ffnd ⊢ ( 𝑑 ∈ ( Poly ‘ 𝐵 ) → 𝑑 Fn ℂ )
79 78 adantl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → 𝑑 Fn ℂ )
80 cnex ⊢ ℂ ∈ V
81 80 a1i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ℂ ∈ V )
82 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → 𝑋 ∈ ℂ )
83 fnfvof ⊢ ( ( ( 𝑒 Fn ℂ ∧ 𝑑 Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑋 ∈ ℂ ) ) → ( ( 𝑒 ∘f + 𝑑 ) ‘ 𝑋 ) = ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) )
84 76 79 81 82 83 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( ( 𝑒 ∘f + 𝑑 ) ‘ 𝑋 ) = ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) )
85 84 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) = ( ( 𝑒 ∘f + 𝑑 ) ‘ 𝑋 ) )
86 fveq1 ⊢ ( 𝑝 = ( 𝑒 ∘f + 𝑑 ) → ( 𝑝 ‘ 𝑋 ) = ( ( 𝑒 ∘f + 𝑑 ) ‘ 𝑋 ) )
87 86 rspceeqv ⊢ ( ( ( 𝑒 ∘f + 𝑑 ) ∈ ( Poly ‘ 𝐵 ) ∧ ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) = ( ( 𝑒 ∘f + 𝑑 ) ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) )
88 73 85 87 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) )
89 oveq2 ⊢ ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) )
90 89 eqeq1d ⊢ ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ( ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) ) )
91 90 rexbidv ⊢ ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) ) )
92 88 91 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
93 92 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
94 oveq1 ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( 𝑏 + 𝑐 ) = ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) )
95 94 eqeq1d ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
96 95 rexbidv ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
97 96 imbi2d ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ↔ ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ) )
98 93 97 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ) )
99 98 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ) )
100 99 3imp ⊢ ( ( 𝜑 ∧ ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) ∧ ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) )
101 49 57 65 100 syl3anb ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ∧ 𝑐 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) )
102 ovex ⊢ ( 𝑏 + 𝑐 ) ∈ V
103 eqeq1 ⊢ ( 𝑎 = ( 𝑏 + 𝑐 ) → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
104 103 rexbidv ⊢ ( 𝑎 = ( 𝑏 + 𝑐 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
105 102 104 elab ⊢ ( ( 𝑏 + 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 + 𝑐 ) = ( 𝑝 ‘ 𝑋 ) )
106 101 105 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ∧ 𝑐 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) → ( 𝑏 + 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
107 ax-1cn ⊢ 1 ∈ ℂ
108 cnfldneg ⊢ ( 1 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 1 ) = - 1 )
109 107 108 mp1i ⊢ ( 𝜑 → ( ( invg ‘ ℂfld ) ‘ 1 ) = - 1 )
110 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
111 110 subrg1cl ⊢ ( 𝐵 ∈ ( SubRing ‘ ℂfld ) → 1 ∈ 𝐵 )
112 1 111 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
113 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
114 113 subginvcl ⊢ ( ( 𝐵 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐵 ) → ( ( invg ‘ ℂfld ) ‘ 1 ) ∈ 𝐵 )
115 45 112 114 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ℂfld ) ‘ 1 ) ∈ 𝐵 )
116 109 115 eqeltrrd ⊢ ( 𝜑 → - 1 ∈ 𝐵 )
117 plyconst ⊢ ( ( 𝐵 ⊆ ℂ ∧ - 1 ∈ 𝐵 ) → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝐵 ) )
118 10 116 117 syl2anc ⊢ ( 𝜑 → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝐵 ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝐵 ) )
120 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → 𝑒 ∈ ( Poly ‘ 𝐵 ) )
121 cnfldmul ⊢ · = ( .r ‘ ℂfld )
122 121 subrgmcl ⊢ ( ( 𝐵 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
123 122 3expb ⊢ ( ( 𝐵 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
124 1 123 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
125 124 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
126 119 120 71 125 plymul ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ∈ ( Poly ‘ 𝐵 ) )
127 ffvelrn ⊢ ( ( 𝑒 : ℂ ⟶ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑒 ‘ 𝑋 ) ∈ ℂ )
128 74 2 127 syl2anr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑒 ‘ 𝑋 ) ∈ ℂ )
129 cnfldneg ⊢ ( ( 𝑒 ‘ 𝑋 ) ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = - ( 𝑒 ‘ 𝑋 ) )
130 128 129 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = - ( 𝑒 ‘ 𝑋 ) )
131 negex ⊢ - 1 ∈ V
132 fnconstg ⊢ ( - 1 ∈ V → ( ℂ × { - 1 } ) Fn ℂ )
133 131 132 mp1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ℂ × { - 1 } ) Fn ℂ )
134 75 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → 𝑒 Fn ℂ )
135 80 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ℂ ∈ V )
136 2 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → 𝑋 ∈ ℂ )
137 fnfvof ⊢ ( ( ( ( ℂ × { - 1 } ) Fn ℂ ∧ 𝑒 Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑋 ∈ ℂ ) ) → ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ‘ 𝑋 ) = ( ( ( ℂ × { - 1 } ) ‘ 𝑋 ) · ( 𝑒 ‘ 𝑋 ) ) )
138 133 134 135 136 137 syl22anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ‘ 𝑋 ) = ( ( ( ℂ × { - 1 } ) ‘ 𝑋 ) · ( 𝑒 ‘ 𝑋 ) ) )
139 131 fvconst2 ⊢ ( 𝑋 ∈ ℂ → ( ( ℂ × { - 1 } ) ‘ 𝑋 ) = - 1 )
140 136 139 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( ℂ × { - 1 } ) ‘ 𝑋 ) = - 1 )
141 140 oveq1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( ( ℂ × { - 1 } ) ‘ 𝑋 ) · ( 𝑒 ‘ 𝑋 ) ) = ( - 1 · ( 𝑒 ‘ 𝑋 ) ) )
142 128 mulm1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( - 1 · ( 𝑒 ‘ 𝑋 ) ) = - ( 𝑒 ‘ 𝑋 ) )
143 138 141 142 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ‘ 𝑋 ) = - ( 𝑒 ‘ 𝑋 ) )
144 130 143 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ‘ 𝑋 ) )
145 fveq1 ⊢ ( 𝑝 = ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) → ( 𝑝 ‘ 𝑋 ) = ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ‘ 𝑋 ) )
146 145 rspceeqv ⊢ ( ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ∈ ( Poly ‘ 𝐵 ) ∧ ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = ( ( ( ℂ × { - 1 } ) ∘f · 𝑒 ) ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) )
147 126 144 146 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) )
148 fveqeq2 ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) ↔ ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) ) )
149 148 rexbidv ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ ( 𝑒 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) ) )
150 147 149 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) ) )
151 150 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) ) )
152 151 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) )
153 57 152 sylan2b ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) )
154 fvex ⊢ ( ( invg ‘ ℂfld ) ‘ 𝑏 ) ∈ V
155 eqeq1 ⊢ ( 𝑎 = ( ( invg ‘ ℂfld ) ‘ 𝑏 ) → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) ) )
156 155 rexbidv ⊢ ( 𝑎 = ( ( invg ‘ ℂfld ) ‘ 𝑏 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) ) )
157 154 156 elab ⊢ ( ( ( invg ‘ ℂfld ) ‘ 𝑏 ) ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( invg ‘ ℂfld ) ‘ 𝑏 ) = ( 𝑝 ‘ 𝑋 ) )
158 153 157 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) → ( ( invg ‘ ℂfld ) ‘ 𝑏 ) ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
159 110 a1i ⊢ ( 𝜑 → 1 = ( 1r ‘ ℂfld ) )
160 121 a1i ⊢ ( 𝜑 → · = ( .r ‘ ℂfld ) )
161 43 112 sseldd ⊢ ( 𝜑 → 1 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
162 125 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
163 66 67 72 162 plymul ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑒 ∘f · 𝑑 ) ∈ ( Poly ‘ 𝐵 ) )
164 fnfvof ⊢ ( ( ( 𝑒 Fn ℂ ∧ 𝑑 Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑋 ∈ ℂ ) ) → ( ( 𝑒 ∘f · 𝑑 ) ‘ 𝑋 ) = ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) )
165 76 79 81 82 164 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( ( 𝑒 ∘f · 𝑑 ) ‘ 𝑋 ) = ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) )
166 165 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) = ( ( 𝑒 ∘f · 𝑑 ) ‘ 𝑋 ) )
167 fveq1 ⊢ ( 𝑝 = ( 𝑒 ∘f · 𝑑 ) → ( 𝑝 ‘ 𝑋 ) = ( ( 𝑒 ∘f · 𝑑 ) ‘ 𝑋 ) )
168 167 rspceeqv ⊢ ( ( ( 𝑒 ∘f · 𝑑 ) ∈ ( Poly ‘ 𝐵 ) ∧ ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) = ( ( 𝑒 ∘f · 𝑑 ) ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) )
169 163 166 168 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) )
170 oveq2 ⊢ ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) )
171 170 eqeq1d ⊢ ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ( ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) ) )
172 171 rexbidv ⊢ ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · ( 𝑑 ‘ 𝑋 ) ) = ( 𝑝 ‘ 𝑋 ) ) )
173 169 172 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) ∧ 𝑑 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
174 173 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
175 oveq1 ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( 𝑏 · 𝑐 ) = ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) )
176 175 eqeq1d ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
177 176 rexbidv ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
178 177 imbi2d ⊢ ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ↔ ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( ( 𝑒 ‘ 𝑋 ) · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ) )
179 174 178 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ) )
180 179 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) → ( ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) ) )
181 180 3imp ⊢ ( ( 𝜑 ∧ ∃ 𝑒 ∈ ( Poly ‘ 𝐵 ) 𝑏 = ( 𝑒 ‘ 𝑋 ) ∧ ∃ 𝑑 ∈ ( Poly ‘ 𝐵 ) 𝑐 = ( 𝑑 ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) )
182 49 57 65 181 syl3anb ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ∧ 𝑐 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) )
183 ovex ⊢ ( 𝑏 · 𝑐 ) ∈ V
184 eqeq1 ⊢ ( 𝑎 = ( 𝑏 · 𝑐 ) → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
185 184 rexbidv ⊢ ( 𝑎 = ( 𝑏 · 𝑐 ) → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) ) )
186 183 185 elab ⊢ ( ( 𝑏 · 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) ( 𝑏 · 𝑐 ) = ( 𝑝 ‘ 𝑋 ) )
187 182 186 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ∧ 𝑐 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) → ( 𝑏 · 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
188 15 17 19 29 48 106 158 159 160 161 187 6 issubrngd2 ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ∈ ( SubRing ‘ ℂfld ) )
189 plyid ⊢ ( ( 𝐵 ⊆ ℂ ∧ 1 ∈ 𝐵 ) → Xp ∈ ( Poly ‘ 𝐵 ) )
190 10 112 189 syl2anc ⊢ ( 𝜑 → Xp ∈ ( Poly ‘ 𝐵 ) )
191 df-idp ⊢ Xp = ( I ↾ ℂ )
192 191 fveq1i ⊢ ( Xp ‘ 𝑋 ) = ( ( I ↾ ℂ ) ‘ 𝑋 )
193 fvresi ⊢ ( 𝑋 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝑋 ) = 𝑋 )
194 2 193 syl ⊢ ( 𝜑 → ( ( I ↾ ℂ ) ‘ 𝑋 ) = 𝑋 )
195 192 194 eqtr2id ⊢ ( 𝜑 → 𝑋 = ( Xp ‘ 𝑋 ) )
196 fveq1 ⊢ ( 𝑝 = Xp → ( 𝑝 ‘ 𝑋 ) = ( Xp ‘ 𝑋 ) )
197 196 rspceeqv ⊢ ( ( Xp ∈ ( Poly ‘ 𝐵 ) ∧ 𝑋 = ( Xp ‘ 𝑋 ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑋 = ( 𝑝 ‘ 𝑋 ) )
198 190 195 197 syl2anc ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑋 = ( 𝑝 ‘ 𝑋 ) )
199 eqeq1 ⊢ ( 𝑎 = 𝑋 → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ 𝑋 = ( 𝑝 ‘ 𝑋 ) ) )
200 199 rexbidv ⊢ ( 𝑎 = 𝑋 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑋 = ( 𝑝 ‘ 𝑋 ) ) )
201 2 198 200 elabd ⊢ ( 𝜑 → 𝑋 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
202 201 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
203 43 202 unssd ⊢ ( 𝜑 → ( 𝐵 ∪ { 𝑋 } ) ⊆ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
204 6 8 12 13 14 188 203 rgspnmin ⊢ ( 𝜑 → ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ⊆ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } )
205 204 sseld ⊢ ( 𝜑 → ( 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) → 𝑉 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ) )
206 fvex ⊢ ( 𝑝 ‘ 𝑋 ) ∈ V
207 eleq1 ⊢ ( 𝑉 = ( 𝑝 ‘ 𝑋 ) → ( 𝑉 ∈ V ↔ ( 𝑝 ‘ 𝑋 ) ∈ V ) )
208 206 207 mpbiri ⊢ ( 𝑉 = ( 𝑝 ‘ 𝑋 ) → 𝑉 ∈ V )
209 208 rexlimivw ⊢ ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) → 𝑉 ∈ V )
210 eqeq1 ⊢ ( 𝑎 = 𝑉 → ( 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ 𝑉 = ( 𝑝 ‘ 𝑋 ) ) )
211 210 rexbidv ⊢ ( 𝑎 = 𝑉 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) ) )
212 209 211 elab3 ⊢ ( 𝑉 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑎 = ( 𝑝 ‘ 𝑋 ) } ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) )
213 205 212 syl6ib ⊢ ( 𝜑 → ( 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) → ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) ) )
214 6 8 12 13 14 rgspncl ⊢ ( 𝜑 → ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ ℂfld ) )
215 214 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ∈ ( SubRing ‘ ℂfld ) )
216 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → 𝑝 ∈ ( Poly ‘ 𝐵 ) )
217 6 8 12 13 14 rgspnssid ⊢ ( 𝜑 → ( 𝐵 ∪ { 𝑋 } ) ⊆ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
218 217 unssbd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
219 snidg ⊢ ( 𝑋 ∈ ℂ → 𝑋 ∈ { 𝑋 } )
220 2 219 syl ⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
221 218 220 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
222 221 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → 𝑋 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
223 217 unssad ⊢ ( 𝜑 → 𝐵 ⊆ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
224 223 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → 𝐵 ⊆ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
225 215 216 222 224 cnsrplycl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑝 ‘ 𝑋 ) ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) )
226 eleq1 ⊢ ( 𝑉 = ( 𝑝 ‘ 𝑋 ) → ( 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ↔ ( 𝑝 ‘ 𝑋 ) ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ) )
227 225 226 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Poly ‘ 𝐵 ) ) → ( 𝑉 = ( 𝑝 ‘ 𝑋 ) → 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ) )
228 227 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) → 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ) )
229 213 228 impbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( 𝐵 ∪ { 𝑋 } ) ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) ) )
230 4 229 bitrd ⊢ ( 𝜑 → ( 𝑉 ∈ 𝑆 ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝐵 ) 𝑉 = ( 𝑝 ‘ 𝑋 ) ) )