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 
|- ( ph -> B e. ( SubRing ` CCfld ) )
rngunsnply.x 
|- ( ph -> X e. CC )
rngunsnply.s 
|- ( ph -> S = ( ( RingSpan ` CCfld ) ` ( B u. { X } ) ) )
Assertion rngunsnply 
|- ( ph -> ( V e. S <-> E. p e. ( Poly ` B ) V = ( p ` X ) ) )

Proof

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