MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pf1ind Structured version   Unicode version

Theorem pf1ind 17789
Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015.)
Hypotheses
Ref Expression
pf1ind.cb  |-  B  =  ( Base `  R
)
pf1ind.cp  |-  .+  =  ( +g  `  R )
pf1ind.ct  |-  .x.  =  ( .r `  R )
pf1ind.cq  |-  Q  =  ran  (eval1 `  R )
pf1ind.ad  |-  ( (
ph  /\  ( (
f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) ) )  ->  ze )
pf1ind.mu  |-  ( (
ph  /\  ( (
f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) ) )  ->  si )
pf1ind.wa  |-  ( x  =  ( B  X.  { f } )  ->  ( ps  <->  ch )
)
pf1ind.wb  |-  ( x  =  (  _I  |`  B )  ->  ( ps  <->  th )
)
pf1ind.wc  |-  ( x  =  f  ->  ( ps 
<->  ta ) )
pf1ind.wd  |-  ( x  =  g  ->  ( ps 
<->  et ) )
pf1ind.we  |-  ( x  =  ( f  oF  .+  g )  ->  ( ps  <->  ze )
)
pf1ind.wf  |-  ( x  =  ( f  oF  .x.  g )  ->  ( ps  <->  si )
)
pf1ind.wg  |-  ( x  =  A  ->  ( ps 
<->  rh ) )
pf1ind.co  |-  ( (
ph  /\  f  e.  B )  ->  ch )
pf1ind.pr  |-  ( ph  ->  th )
pf1ind.a  |-  ( ph  ->  A  e.  Q )
Assertion
Ref Expression
pf1ind  |-  ( ph  ->  rh )
Distinct variable groups:    f, g, x,  .+    B, f, g, x    et, f, x    ph, f,
g    x, A    ch, x    ps, f, g    Q, f, g    rh, x    si, x    ta, x    th, x    .x. , f, g, x    ze, x
Allowed substitution hints:    ph( x)    ps( x)    ch( f, g)    th( f,
g)    ta( f, g)    et( g)    ze( f, g)    si( f,
g)    rh( f, g)    A( f, g)    Q( x)    R( x, f, g)

Proof of Theorem pf1ind
Dummy variables  a 
b  y  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 coass 5356 . . . . 5  |-  ( ( A  o.  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  =  ( A  o.  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
2 df1o2 6932 . . . . . . . . 9  |-  1o  =  { (/) }
3 pf1ind.cb . . . . . . . . . 10  |-  B  =  ( Base `  R
)
4 fvex 5701 . . . . . . . . . 10  |-  ( Base `  R )  e.  _V
53, 4eqeltri 2513 . . . . . . . . 9  |-  B  e. 
_V
6 0ex 4422 . . . . . . . . 9  |-  (/)  e.  _V
7 eqid 2443 . . . . . . . . 9  |-  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) )  =  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) )
82, 5, 6, 7mapsncnv 7259 . . . . . . . 8  |-  `' ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  =  ( w  e.  B  |->  ( 1o  X.  { w } ) )
98coeq2i 5000 . . . . . . 7  |-  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  `' ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) )  =  ( ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )
102, 5, 6, 7mapsnf1o2 7260 . . . . . . . 8  |-  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) : ( B  ^m  1o )
-1-1-onto-> B
11 f1ococnv2 5667 . . . . . . . 8  |-  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) ) : ( B  ^m  1o ) -1-1-onto-> B  ->  ( (
b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  `' ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) )  =  (  _I  |`  B ) )
1210, 11mp1i 12 . . . . . . 7  |-  ( ph  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  `' ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  =  (  _I  |`  B ) )
139, 12syl5eqr 2489 . . . . . 6  |-  ( ph  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  =  (  _I  |`  B ) )
1413coeq2d 5002 . . . . 5  |-  ( ph  ->  ( A  o.  (
( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  =  ( A  o.  (  _I  |`  B ) ) )
151, 14syl5eq 2487 . . . 4  |-  ( ph  ->  ( ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  =  ( A  o.  (  _I  |`  B ) ) )
16 pf1ind.a . . . . 5  |-  ( ph  ->  A  e.  Q )
17 pf1ind.cq . . . . . 6  |-  Q  =  ran  (eval1 `  R )
1817, 3pf1f 17784 . . . . 5  |-  ( A  e.  Q  ->  A : B --> B )
19 fcoi1 5585 . . . . 5  |-  ( A : B --> B  -> 
( A  o.  (  _I  |`  B ) )  =  A )
2016, 18, 193syl 20 . . . 4  |-  ( ph  ->  ( A  o.  (  _I  |`  B ) )  =  A )
2115, 20eqtrd 2475 . . 3  |-  ( ph  ->  ( ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  =  A )
22 pf1ind.cp . . . 4  |-  .+  =  ( +g  `  R )
23 pf1ind.ct . . . 4  |-  .x.  =  ( .r `  R )
24 eqid 2443 . . . . . 6  |-  ( 1o eval  R )  =  ( 1o eval  R )
2524, 3evlval 17610 . . . . 5  |-  ( 1o eval  R )  =  ( ( 1o evalSub  R ) `  B )
2625rneqi 5066 . . . 4  |-  ran  ( 1o eval  R )  =  ran  ( ( 1o evalSub  R ) `
 B )
27 an4 820 . . . . . 6  |-  ( ( ( a  e.  ran  ( 1o eval  R )  /\  ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )  /\  ( b  e.  ran  ( 1o eval  R )  /\  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } ) )  <-> 
( ( a  e. 
ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) )  /\  ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps }  /\  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) ) )
28 eqid 2443 . . . . . . . . . . . 12  |-  ran  ( 1o eval  R )  =  ran  ( 1o eval  R )
2917, 3, 28mpfpf1 17785 . . . . . . . . . . 11  |-  ( a  e.  ran  ( 1o eval  R )  ->  (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e.  Q )
3017, 3, 28mpfpf1 17785 . . . . . . . . . . 11  |-  ( b  e.  ran  ( 1o eval  R )  ->  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e.  Q )
31 vex 2975 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
32 pf1ind.wc . . . . . . . . . . . . . . . . 17  |-  ( x  =  f  ->  ( ps 
<->  ta ) )
3331, 32elab 3106 . . . . . . . . . . . . . . . 16  |-  ( f  e.  { x  |  ps }  <->  ta )
34 eleq1 2503 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( f  e.  { x  |  ps } 
<->  ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } ) )
3533, 34syl5bbr 259 . . . . . . . . . . . . . . 15  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( ta  <->  ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )
3635anbi1d 704 . . . . . . . . . . . . . 14  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( ( ta  /\  et )  <->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps }  /\  et ) ) )
3736anbi1d 704 . . . . . . . . . . . . 13  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( ta  /\  et )  /\  ph )  <->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  /\  et )  /\  ph ) ) )
38 ovex 6116 . . . . . . . . . . . . . . 15  |-  ( f  oF  .+  g
)  e.  _V
39 pf1ind.we . . . . . . . . . . . . . . 15  |-  ( x  =  ( f  oF  .+  g )  ->  ( ps  <->  ze )
)
4038, 39elab 3106 . . . . . . . . . . . . . 14  |-  ( ( f  oF  .+  g )  e.  {
x  |  ps }  <->  ze )
41 oveq1 6098 . . . . . . . . . . . . . . 15  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( f  oF  .+  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  g ) )
4241eleq1d 2509 . . . . . . . . . . . . . 14  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
f  oF  .+  g )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  g
)  e.  { x  |  ps } ) )
4340, 42syl5bbr 259 . . . . . . . . . . . . 13  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( ze  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  g
)  e.  { x  |  ps } ) )
4437, 43imbi12d 320 . . . . . . . . . . . 12  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( ( ta  /\  et )  /\  ph )  ->  ze )  <->  ( (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  et )  /\  ph )  -> 
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  oF  .+  g )  e.  {
x  |  ps }
) ) )
45 vex 2975 . . . . . . . . . . . . . . . . 17  |-  g  e. 
_V
46 pf1ind.wd . . . . . . . . . . . . . . . . 17  |-  ( x  =  g  ->  ( ps 
<->  et ) )
4745, 46elab 3106 . . . . . . . . . . . . . . . 16  |-  ( g  e.  { x  |  ps }  <->  et )
48 eleq1 2503 . . . . . . . . . . . . . . . 16  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( g  e.  { x  |  ps } 
<->  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } ) )
4947, 48syl5bbr 259 . . . . . . . . . . . . . . 15  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( et  <->  ( b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )
5049anbi2d 703 . . . . . . . . . . . . . 14  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  /\  et ) 
<->  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) ) )
5150anbi1d 704 . . . . . . . . . . . . 13  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  et )  /\  ph )  <->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  ph ) ) )
52 oveq2 6099 . . . . . . . . . . . . . 14  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .+  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) ) )
5352eleq1d 2509 . . . . . . . . . . . . 13  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  g
)  e.  { x  |  ps }  <->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
5451, 53imbi12d 320 . . . . . . . . . . . 12  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  /\  et )  /\  ph )  ->  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  g )  e. 
{ x  |  ps } )  <->  ( (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  ph )  ->  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) )  e.  {
x  |  ps }
) ) )
55 pf1ind.ad . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) ) )  ->  ze )
5655expcom 435 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) )  ->  ( ph  ->  ze ) )
5756an4s 822 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  Q  /\  g  e.  Q
)  /\  ( ta  /\  et ) )  -> 
( ph  ->  ze )
)
5857expimpd 603 . . . . . . . . . . . 12  |-  ( ( f  e.  Q  /\  g  e.  Q )  ->  ( ( ( ta 
/\  et )  /\  ph )  ->  ze )
)
5944, 54, 58vtocl2ga 3038 . . . . . . . . . . 11  |-  ( ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  Q  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e.  Q )  ->  (
( ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  /\  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )  /\  ph )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
6029, 30, 59syl2an 477 . . . . . . . . . 10  |-  ( ( a  e.  ran  ( 1o eval  R )  /\  b  e.  ran  ( 1o eval  R
) )  ->  (
( ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  /\  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )  /\  ph )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
6160expcomd 438 . . . . . . . . 9  |-  ( ( a  e.  ran  ( 1o eval  R )  /\  b  e.  ran  ( 1o eval  R
) )  ->  ( ph  ->  ( ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps }  /\  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } )  -> 
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  oF  .+  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e.  { x  |  ps } ) ) )
6261impcom 430 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  ->  (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
6326, 3mpff 17619 . . . . . . . . . . . 12  |-  ( a  e.  ran  ( 1o eval  R )  ->  a : ( B  ^m  1o ) --> B )
6463ad2antrl 727 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  a : ( B  ^m  1o ) --> B )
65 ffn 5559 . . . . . . . . . . 11  |-  ( a : ( B  ^m  1o ) --> B  ->  a  Fn  ( B  ^m  1o ) )
6664, 65syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  a  Fn  ( B  ^m  1o ) )
6726, 3mpff 17619 . . . . . . . . . . . 12  |-  ( b  e.  ran  ( 1o eval  R )  ->  b : ( B  ^m  1o ) --> B )
6867ad2antll 728 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  b : ( B  ^m  1o ) --> B )
69 ffn 5559 . . . . . . . . . . 11  |-  ( b : ( B  ^m  1o ) --> B  ->  b  Fn  ( B  ^m  1o ) )
7068, 69syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  b  Fn  ( B  ^m  1o ) )
71 eqid 2443 . . . . . . . . . . . 12  |-  ( w  e.  B  |->  ( 1o 
X.  { w }
) )  =  ( w  e.  B  |->  ( 1o  X.  { w } ) )
722, 5, 6, 71mapsnf1o3 7261 . . . . . . . . . . 11  |-  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) : B -1-1-onto-> ( B  ^m  1o )
73 f1of 5641 . . . . . . . . . . 11  |-  ( ( w  e.  B  |->  ( 1o  X.  { w } ) ) : B -1-1-onto-> ( B  ^m  1o )  ->  ( w  e.  B  |->  ( 1o  X.  { w } ) ) : B --> ( B  ^m  1o ) )
7472, 73mp1i 12 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
w  e.  B  |->  ( 1o  X.  { w } ) ) : B --> ( B  ^m  1o ) )
75 ovex 6116 . . . . . . . . . . 11  |-  ( B  ^m  1o )  e. 
_V
7675a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  ( B  ^m  1o )  e. 
_V )
775a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  B  e.  _V )
78 inidm 3559 . . . . . . . . . 10  |-  ( ( B  ^m  1o )  i^i  ( B  ^m  1o ) )  =  ( B  ^m  1o )
7966, 70, 74, 76, 76, 77, 78ofco 6340 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( a  oF  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) ) )
8079eleq1d 2509 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  oF  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .+  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
8162, 80sylibrd 234 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  ->  (
( a  oF  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
8281expimpd 603 . . . . . 6  |-  ( ph  ->  ( ( ( a  e.  ran  ( 1o eval  R )  /\  b  e.  ran  ( 1o eval  R
) )  /\  (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )  -> 
( ( a  oF  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
8327, 82syl5bi 217 . . . . 5  |-  ( ph  ->  ( ( ( a  e.  ran  ( 1o eval  R )  /\  (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  (
b  e.  ran  ( 1o eval  R )  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )  -> 
( ( a  oF  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
8483imp 429 . . . 4  |-  ( (
ph  /\  ( (
a  e.  ran  ( 1o eval  R )  /\  (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  (
b  e.  ran  ( 1o eval  R )  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) ) )  ->  ( ( a  oF  .+  b
)  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
85 ovex 6116 . . . . . . . . . . . . . . 15  |-  ( f  oF  .x.  g
)  e.  _V
86 pf1ind.wf . . . . . . . . . . . . . . 15  |-  ( x  =  ( f  oF  .x.  g )  ->  ( ps  <->  si )
)
8785, 86elab 3106 . . . . . . . . . . . . . 14  |-  ( ( f  oF  .x.  g )  e.  {
x  |  ps }  <->  si )
88 oveq1 6098 . . . . . . . . . . . . . . 15  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( f  oF  .x.  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  g ) )
8988eleq1d 2509 . . . . . . . . . . . . . 14  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
f  oF  .x.  g )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  g
)  e.  { x  |  ps } ) )
9087, 89syl5bbr 259 . . . . . . . . . . . . 13  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( si  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  g
)  e.  { x  |  ps } ) )
9137, 90imbi12d 320 . . . . . . . . . . . 12  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( ( ta  /\  et )  /\  ph )  ->  si )  <->  ( (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  et )  /\  ph )  -> 
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  oF  .x.  g )  e.  {
x  |  ps }
) ) )
92 oveq2 6099 . . . . . . . . . . . . . 14  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .x.  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) ) )
9392eleq1d 2509 . . . . . . . . . . . . 13  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  g
)  e.  { x  |  ps }  <->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
9451, 93imbi12d 320 . . . . . . . . . . . 12  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  /\  et )  /\  ph )  ->  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  g )  e. 
{ x  |  ps } )  <->  ( (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  ph )  ->  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) )  e.  {
x  |  ps }
) ) )
95 pf1ind.mu . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) ) )  ->  si )
9695expcom 435 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) )  ->  ( ph  ->  si ) )
9796an4s 822 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  Q  /\  g  e.  Q
)  /\  ( ta  /\  et ) )  -> 
( ph  ->  si )
)
9897expimpd 603 . . . . . . . . . . . 12  |-  ( ( f  e.  Q  /\  g  e.  Q )  ->  ( ( ( ta 
/\  et )  /\  ph )  ->  si )
)
9991, 94, 98vtocl2ga 3038 . . . . . . . . . . 11  |-  ( ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  Q  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e.  Q )  ->  (
( ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  /\  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )  /\  ph )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
10029, 30, 99syl2an 477 . . . . . . . . . 10  |-  ( ( a  e.  ran  ( 1o eval  R )  /\  b  e.  ran  ( 1o eval  R
) )  ->  (
( ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  /\  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )  /\  ph )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
101100expcomd 438 . . . . . . . . 9  |-  ( ( a  e.  ran  ( 1o eval  R )  /\  b  e.  ran  ( 1o eval  R
) )  ->  ( ph  ->  ( ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps }  /\  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } )  -> 
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  oF  .x.  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e.  { x  |  ps } ) ) )
102101impcom 430 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  ->  (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
10366, 70, 74, 76, 76, 77, 78ofco 6340 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( a  oF  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  oF  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) ) )
104103eleq1d 2509 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  oF  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  oF  .x.  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
105102, 104sylibrd 234 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  ->  (
( a  oF  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
106105expimpd 603 . . . . . 6  |-  ( ph  ->  ( ( ( a  e.  ran  ( 1o eval  R )  /\  b  e.  ran  ( 1o eval  R
) )  /\  (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )  -> 
( ( a  oF  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
10727, 106syl5bi 217 . . . . 5  |-  ( ph  ->  ( ( ( a  e.  ran  ( 1o eval  R )  /\  (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  (
b  e.  ran  ( 1o eval  R )  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )  -> 
( ( a  oF  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
108107imp 429 . . . 4  |-  ( (
ph  /\  ( (
a  e.  ran  ( 1o eval  R )  /\  (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )  /\  (
b  e.  ran  ( 1o eval  R )  /\  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) ) )  ->  ( ( a  oF  .x.  b
)  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
109 coeq1 4997 . . . . 5  |-  ( y  =  ( ( B  ^m  1o )  X. 
{ a } )  ->  ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( ( B  ^m  1o )  X.  { a } )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )
110109eleq1d 2509 . . . 4  |-  ( y  =  ( ( B  ^m  1o )  X. 
{ a } )  ->  ( ( y  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( ( B  ^m  1o )  X.  { a } )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } ) )
111 coeq1 4997 . . . . 5  |-  ( y  =  ( b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  -> 
( y  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  =  ( ( b  e.  ( B  ^m  1o )  |->  ( b `
 a ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
112111eleq1d 2509 . . . 4  |-  ( y  =  ( b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  -> 
( ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  <->  ( (
b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )
113 coeq1 4997 . . . . 5  |-  ( y  =  a  ->  (
y  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  =  ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
114113eleq1d 2509 . . . 4  |-  ( y  =  a  ->  (
( y  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  <->  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
115 coeq1 4997 . . . . 5  |-  ( y  =  b  ->  (
y  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  =  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
116115eleq1d 2509 . . . 4  |-  ( y  =  b  ->  (
( y  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps }  <->  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
117 coeq1 4997 . . . . 5  |-  ( y  =  ( a  oF  .+  b )  ->  ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  oF  .+  b )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
118117eleq1d 2509 . . . 4  |-  ( y  =  ( a  oF  .+  b )  ->  ( ( y  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  oF  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
119 coeq1 4997 . . . . 5  |-  ( y  =  ( a  oF  .x.  b )  ->  ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  oF  .x.  b )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
120119eleq1d 2509 . . . 4  |-  ( y  =  ( a  oF  .x.  b )  ->  ( ( y  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  oF  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
121 coeq1 4997 . . . . 5  |-  ( y  =  ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  ->  ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( A  o.  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
122121eleq1d 2509 . . . 4  |-  ( y  =  ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  ->  ( (
y  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } 
<->  ( ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )
12317pf1rcl 17783 . . . . . . . . 9  |-  ( A  e.  Q  ->  R  e.  CRing )
12416, 123syl 16 . . . . . . . 8  |-  ( ph  ->  R  e.  CRing )
125124adantr 465 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  R  e.  CRing )
126 1on 6927 . . . . . . . . . . . 12  |-  1o  e.  On
127 eqid 2443 . . . . . . . . . . . . 13  |-  ( 1o mPoly  R )  =  ( 1o mPoly  R )
128127mplassa 17533 . . . . . . . . . . . 12  |-  ( ( 1o  e.  On  /\  R  e.  CRing )  -> 
( 1o mPoly  R )  e. AssAlg )
129126, 124, 128sylancr 663 . . . . . . . . . . 11  |-  ( ph  ->  ( 1o mPoly  R )  e. AssAlg )
130 eqid 2443 . . . . . . . . . . . . 13  |-  (Poly1 `  R
)  =  (Poly1 `  R
)
131 eqid 2443 . . . . . . . . . . . . 13  |-  (algSc `  (Poly1 `  R ) )  =  (algSc `  (Poly1 `  R
) )
132130, 131ply1ascl 17712 . . . . . . . . . . . 12  |-  (algSc `  (Poly1 `  R ) )  =  (algSc `  ( 1o mPoly  R ) )
133 eqid 2443 . . . . . . . . . . . 12  |-  (Scalar `  ( 1o mPoly  R ) )  =  (Scalar `  ( 1o mPoly  R ) )
134132, 133asclrhm 17412 . . . . . . . . . . 11  |-  ( ( 1o mPoly  R )  e. AssAlg  ->  (algSc `  (Poly1 `  R
) )  e.  ( (Scalar `  ( 1o mPoly  R ) ) RingHom  ( 1o mPoly  R ) ) )
135129, 134syl 16 . . . . . . . . . 10  |-  ( ph  ->  (algSc `  (Poly1 `  R
) )  e.  ( (Scalar `  ( 1o mPoly  R ) ) RingHom  ( 1o mPoly  R ) ) )
136126a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  1o  e.  On )
137127, 136, 124mplsca 17524 . . . . . . . . . . 11  |-  ( ph  ->  R  =  (Scalar `  ( 1o mPoly  R ) ) )
138137oveq1d 6106 . . . . . . . . . 10  |-  ( ph  ->  ( R RingHom  ( 1o mPoly  R ) )  =  ( (Scalar `  ( 1o mPoly  R ) ) RingHom  ( 1o mPoly  R ) ) )
139135, 138eleqtrrd 2520 . . . . . . . . 9  |-  ( ph  ->  (algSc `  (Poly1 `  R
) )  e.  ( R RingHom  ( 1o mPoly  R
) ) )
140 eqid 2443 . . . . . . . . . 10  |-  ( Base `  ( 1o mPoly  R )
)  =  ( Base `  ( 1o mPoly  R )
)
1413, 140rhmf 16816 . . . . . . . . 9  |-  ( (algSc `  (Poly1 `  R ) )  e.  ( R RingHom  ( 1o mPoly  R ) )  -> 
(algSc `  (Poly1 `  R
) ) : B --> ( Base `  ( 1o mPoly  R ) ) )
142139, 141syl 16 . . . . . . . 8  |-  ( ph  ->  (algSc `  (Poly1 `  R
) ) : B --> ( Base `  ( 1o mPoly  R ) ) )
143142ffvelrnda 5843 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  (
(algSc `  (Poly1 `  R
) ) `  a
)  e.  ( Base `  ( 1o mPoly  R )
) )
144 eqid 2443 . . . . . . . 8  |-  (eval1 `  R
)  =  (eval1 `  R
)
145144, 24, 3, 127, 140evl1val 17763 . . . . . . 7  |-  ( ( R  e.  CRing  /\  (
(algSc `  (Poly1 `  R
) ) `  a
)  e.  ( Base `  ( 1o mPoly  R )
) )  ->  (
(eval1 `
 R ) `  ( (algSc `  (Poly1 `  R
) ) `  a
) )  =  ( ( ( 1o eval  R
) `  ( (algSc `  (Poly1 `  R ) ) `
 a ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
146125, 143, 145syl2anc 661 . . . . . 6  |-  ( (
ph  /\  a  e.  B )  ->  (
(eval1 `
 R ) `  ( (algSc `  (Poly1 `  R
) ) `  a
) )  =  ( ( ( 1o eval  R
) `  ( (algSc `  (Poly1 `  R ) ) `
 a ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
147144, 130, 3, 131evl1sca 17768 . . . . . . 7  |-  ( ( R  e.  CRing  /\  a  e.  B )  ->  (
(eval1 `
 R ) `  ( (algSc `  (Poly1 `  R
) ) `  a
) )  =  ( B  X.  { a } ) )
148124, 147sylan 471 . . . . . 6  |-  ( (
ph  /\  a  e.  B )  ->  (
(eval1 `
 R ) `  ( (algSc `  (Poly1 `  R
) ) `  a
) )  =  ( B  X.  { a } ) )
1493ressid 14233 . . . . . . . . . . . . . 14  |-  ( R  e.  CRing  ->  ( Rs  B
)  =  R )
150125, 149syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  B )  ->  ( Rs  B )  =  R )
151150oveq2d 6107 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  B )  ->  ( 1o mPoly  ( Rs  B ) )  =  ( 1o mPoly  R )
)
152151fveq2d 5695 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  B )  ->  (algSc `  ( 1o mPoly  ( Rs  B
) ) )  =  (algSc `  ( 1o mPoly  R ) ) )
153152, 132syl6eqr 2493 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  B )  ->  (algSc `  ( 1o mPoly  ( Rs  B
) ) )  =  (algSc `  (Poly1 `  R
) ) )
154153fveq1d 5693 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  (
(algSc `  ( 1o mPoly  ( Rs  B ) ) ) `
 a )  =  ( (algSc `  (Poly1 `  R ) ) `  a ) )
155154fveq2d 5695 . . . . . . . 8  |-  ( (
ph  /\  a  e.  B )  ->  (
( 1o eval  R ) `  ( (algSc `  ( 1o mPoly  ( Rs  B ) ) ) `
 a ) )  =  ( ( 1o eval  R ) `  (
(algSc `  (Poly1 `  R
) ) `  a
) ) )
156 eqid 2443 . . . . . . . . 9  |-  ( 1o mPoly 
( Rs  B ) )  =  ( 1o mPoly  ( Rs  B
) )
157 eqid 2443 . . . . . . . . 9  |-  ( Rs  B )  =  ( Rs  B )
158 eqid 2443 . . . . . . . . 9  |-  (algSc `  ( 1o mPoly  ( Rs  B
) ) )  =  (algSc `  ( 1o mPoly  ( Rs  B ) ) )
159126a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  1o  e.  On )
160 crngrng 16655 . . . . . . . . . . 11  |-  ( R  e.  CRing  ->  R  e.  Ring )
1613subrgid 16867 . . . . . . . . . . 11  |-  ( R  e.  Ring  ->  B  e.  (SubRing `  R )
)
162124, 160, 1613syl 20 . . . . . . . . . 10  |-  ( ph  ->  B  e.  (SubRing `  R
) )
163162adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  B  e.  (SubRing `  R )
)
164 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  a  e.  B )
16525, 156, 157, 3, 158, 159, 125, 163, 164evlssca 17608 . . . . . . . 8  |-  ( (
ph  /\  a  e.  B )  ->  (
( 1o eval  R ) `  ( (algSc `  ( 1o mPoly  ( Rs  B ) ) ) `
 a ) )  =  ( ( B  ^m  1o )  X. 
{ a } ) )
166155, 165eqtr3d 2477 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  (
( 1o eval  R ) `  ( (algSc `  (Poly1 `  R ) ) `  a ) )  =  ( ( B  ^m  1o )  X.  { a } ) )
167166coeq1d 5001 . . . . . 6  |-  ( (
ph  /\  a  e.  B )  ->  (
( ( 1o eval  R
) `  ( (algSc `  (Poly1 `  R ) ) `
 a ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  =  ( ( ( B  ^m  1o )  X.  { a } )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
168146, 148, 1673eqtr3d 2483 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  ( B  X.  { a } )  =  ( ( ( B  ^m  1o )  X.  { a } )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )
169 pf1ind.co . . . . . . . 8  |-  ( (
ph  /\  f  e.  B )  ->  ch )
170 snex 4533 . . . . . . . . . 10  |-  { f }  e.  _V
1715, 170xpex 6508 . . . . . . . . 9  |-  ( B  X.  { f } )  e.  _V
172 pf1ind.wa . . . . . . . . 9  |-  ( x  =  ( B  X.  { f } )  ->  ( ps  <->  ch )
)
173171, 172elab 3106 . . . . . . . 8  |-  ( ( B  X.  { f } )  e.  {
x  |  ps }  <->  ch )
174169, 173sylibr 212 . . . . . . 7  |-  ( (
ph  /\  f  e.  B )  ->  ( B  X.  { f } )  e.  { x  |  ps } )
175174ralrimiva 2799 . . . . . 6  |-  ( ph  ->  A. f  e.  B  ( B  X.  { f } )  e.  {
x  |  ps }
)
176 sneq 3887 . . . . . . . . 9  |-  ( f  =  a  ->  { f }  =  { a } )
177176xpeq2d 4864 . . . . . . . 8  |-  ( f  =  a  ->  ( B  X.  { f } )  =  ( B  X.  { a } ) )
178177eleq1d 2509 . . . . . . 7  |-  ( f  =  a  ->  (
( B  X.  {
f } )  e. 
{ x  |  ps } 
<->  ( B  X.  {
a } )  e. 
{ x  |  ps } ) )
179178rspccva 3072 . . . . . 6  |-  ( ( A. f  e.  B  ( B  X.  { f } )  e.  {
x  |  ps }  /\  a  e.  B
)  ->  ( B  X.  { a } )  e.  { x  |  ps } )
180175, 179sylan 471 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  ( B  X.  { a } )  e.  { x  |  ps } )
181168, 180eqeltrrd 2518 . . . 4  |-  ( (
ph  /\  a  e.  B )  ->  (
( ( B  ^m  1o )  X.  { a } )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )
182 pf1ind.pr . . . . . . . 8  |-  ( ph  ->  th )
183 resiexg 6514 . . . . . . . . . 10  |-  ( B  e.  _V  ->  (  _I  |`  B )  e. 
_V )
1845, 183ax-mp 5 . . . . . . . . 9  |-  (  _I  |`  B )  e.  _V
185 pf1ind.wb . . . . . . . . 9  |-  ( x  =  (  _I  |`  B )  ->  ( ps  <->  th )
)
186184, 185elab 3106 . . . . . . . 8  |-  ( (  _I  |`  B )  e.  { x  |  ps } 
<->  th )
187182, 186sylibr 212 . . . . . . 7  |-  ( ph  ->  (  _I  |`  B )  e.  { x  |  ps } )
18813, 187eqeltrd 2517 . . . . . 6  |-  ( ph  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )
189 el1o 6939 . . . . . . . . . 10  |-  ( a  e.  1o  <->  a  =  (/) )
190 fveq2 5691 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( b `
 a )  =  ( b `  (/) ) )
191189, 190sylbi 195 . . . . . . . . 9  |-  ( a  e.  1o  ->  (
b `  a )  =  ( b `  (/) ) )
192191mpteq2dv 4379 . . . . . . . 8  |-  ( a  e.  1o  ->  (
b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  =  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) )
193192coeq1d 5001 . . . . . . 7  |-  ( a  e.  1o  ->  (
( b  e.  ( B  ^m  1o ) 
|->  ( b `  a
) )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  =  ( ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) )
194193eleq1d 2509 . . . . . 6  |-  ( a  e.  1o  ->  (
( ( b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps }  <->  ( (
b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
195188, 194syl5ibrcom 222 . . . . 5  |-  ( ph  ->  ( a  e.  1o  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
196195imp 429 . . . 4  |-  ( (
ph  /\  a  e.  1o )  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
19717, 3, 28pf1mpf 17786 . . . . 5  |-  ( A  e.  Q  ->  ( A  o.  ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) ) )  e. 
ran  ( 1o eval  R
) )
19816, 197syl 16 . . . 4  |-  ( ph  ->  ( A  o.  (
b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) ) )  e.  ran  ( 1o eval  R ) )
1993, 22, 23, 26, 84, 108, 110, 112, 114, 116, 118, 120, 122, 181, 196, 198mpfind 17622 . . 3  |-  ( ph  ->  ( ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
20021, 199eqeltrrd 2518 . 2  |-  ( ph  ->  A  e.  { x  |  ps } )
201 pf1ind.wg . . . 4  |-  ( x  =  A  ->  ( ps 
<->  rh ) )
202201elabg 3107 . . 3  |-  ( A  e.  Q  ->  ( A  e.  { x  |  ps }  <->  rh )
)
20316, 202syl 16 . 2  |-  ( ph  ->  ( A  e.  {
x  |  ps }  <->  rh ) )
204200, 203mpbid 210 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   {cab 2429   A.wral 2715   _Vcvv 2972   (/)c0 3637   {csn 3877    e. cmpt 4350    _I cid 4631   Oncon0 4719    X. cxp 4838   `'ccnv 4839   ran crn 4841    |` cres 4842    o. ccom 4844    Fn wfn 5413   -->wf 5414   -1-1-onto->wf1o 5417   ` cfv 5418  (class class class)co 6091    oFcof 6318   1oc1o 6913    ^m cmap 7214   Basecbs 14174   ↾s cress 14175   +g cplusg 14238   .rcmulr 14239  Scalarcsca 14241   Ringcrg 16645   CRingccrg 16646   RingHom crh 16804  SubRingcsubrg 16861  AssAlgcasa 17381  algSccascl 17383   mPoly cmpl 17420   evalSub ces 17586   eval cevl 17587  Poly1cpl1 17633  eval1ce1 17749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-inf2 7847  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-iin 4174  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-se 4680  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-isom 5427  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-of 6320  df-ofr 6321  df-om 6477  df-1st 6577  df-2nd 6578  df-supp 6691  df-recs 6832  df-rdg 6866  df-1o 6920  df-2o 6921  df-oadd 6924  df-er 7101  df-map 7216  df-pm 7217  df-ixp 7264  df-en 7311  df-dom 7312  df-sdom 7313  df-fin 7314  df-fsupp 7621  df-sup 7691  df-oi 7724  df-card 8109  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-nn 10323  df-2 10380  df-3 10381  df-4 10382  df-5 10383  df-6 10384  df-7 10385  df-8 10386  df-9 10387  df-10 10388  df-n0 10580  df-z 10647  df-dec 10756  df-uz 10862  df-fz 11438  df-fzo 11549  df-seq 11807  df-hash 12104  df-struct 14176  df-ndx 14177  df-slot 14178  df-base 14179  df-sets 14180  df-ress 14181  df-plusg 14251  df-mulr 14252  df-sca 14254  df-vsca 14255  df-ip 14256  df-tset 14257  df-ple 14258  df-ds 14260  df-hom 14262  df-cco 14263  df-0g 14380  df-gsum 14381  df-prds 14386  df-pws 14388  df-mre 14524  df-mrc 14525  df-acs 14527  df-mnd 15415  df-mhm 15464  df-submnd 15465  df-grp 15545  df-minusg 15546  df-sbg 15547  df-mulg 15548  df-subg 15678  df-ghm 15745  df-cntz 15835  df-cmn 16279  df-abl 16280  df-mgp 16592  df-ur 16604  df-srg 16608  df-rng 16647  df-cring 16648  df-rnghom 16806  df-subrg 16863  df-lmod 16950  df-lss 17014  df-lsp 17053  df-assa 17384  df-asp 17385  df-ascl 17386  df-psr 17423  df-mvr 17424  df-mpl 17425  df-opsr 17427  df-evls 17588  df-evl 17589  df-psr1 17636  df-ply1 17638  df-evl1 17751
This theorem is referenced by:  pl1cn  26385
  Copyright terms: Public domain W3C validator