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

Theorem pf1ind 19842
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  o F  .+  g )  ->  ( ps  <->  ze )
)
pf1ind.wf  |-  ( x  =  ( f  o F  .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 5328 . . . . 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 6672 . . . . . . . . 9  |-  1o  =  { (/) }
3 pf1ind.cb . . . . . . . . . 10  |-  B  =  ( Base `  R
)
4 fvex 5682 . . . . . . . . . 10  |-  ( Base `  R )  e.  _V
53, 4eqeltri 2457 . . . . . . . . 9  |-  B  e. 
_V
6 0ex 4280 . . . . . . . . 9  |-  (/)  e.  _V
7 eqid 2387 . . . . . . . . 9  |-  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) )  =  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) )
82, 5, 6, 7mapsncnv 6996 . . . . . . . 8  |-  `' ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  =  ( w  e.  B  |->  ( 1o  X.  { w } ) )
98coeq2i 4973 . . . . . . 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 6997 . . . . . . . 8  |-  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) : ( B  ^m  1o )
-1-1-onto-> B
11 f1ococnv2 5642 . . . . . . . 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 2433 . . . . . 6  |-  ( ph  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  =  (  _I  |`  B ) )
1413coeq2d 4975 . . . . 5  |-  ( ph  ->  ( A  o.  (
( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  =  ( A  o.  (  _I  |`  B ) ) )
151, 14syl5eq 2431 . . . 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 19837 . . . . 5  |-  ( A  e.  Q  ->  A : B --> B )
19 fcoi1 5557 . . . . 5  |-  ( A : B --> B  -> 
( A  o.  (  _I  |`  B ) )  =  A )
2016, 18, 193syl 19 . . . 4  |-  ( ph  ->  ( A  o.  (  _I  |`  B ) )  =  A )
2115, 20eqtrd 2419 . . 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 2387 . . . . . 6  |-  ( 1o eval  R )  =  ( 1o eval  R )
2524, 3evlval 19812 . . . . 5  |-  ( 1o eval  R )  =  ( ( 1o evalSub  R ) `  B )
2625rneqi 5036 . . . 4  |-  ran  ( 1o eval  R )  =  ran  ( ( 1o evalSub  R ) `
 B )
27 an4 798 . . . . . 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 2387 . . . . . . . . . . . 12  |-  ran  ( 1o eval  R )  =  ran  ( 1o eval  R )
2917, 3, 28mpfpf1 19838 . . . . . . . . . . 11  |-  ( a  e.  ran  ( 1o eval  R )  ->  (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e.  Q )
3017, 3, 28mpfpf1 19838 . . . . . . . . . . 11  |-  ( b  e.  ran  ( 1o eval  R )  ->  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e.  Q )
31 vex 2902 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
32 pf1ind.wc . . . . . . . . . . . . . . . . 17  |-  ( x  =  f  ->  ( ps 
<->  ta ) )
3331, 32elab 3025 . . . . . . . . . . . . . . . 16  |-  ( f  e.  { x  |  ps }  <->  ta )
34 eleq1 2447 . . . . . . . . . . . . . . . 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 251 . . . . . . . . . . . . . . 15  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( ta  <->  ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )
3635anbi1d 686 . . . . . . . . . . . . . 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 686 . . . . . . . . . . . . 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 6045 . . . . . . . . . . . . . . 15  |-  ( f  o F  .+  g
)  e.  _V
39 pf1ind.we . . . . . . . . . . . . . . 15  |-  ( x  =  ( f  o F  .+  g )  ->  ( ps  <->  ze )
)
4038, 39elab 3025 . . . . . . . . . . . . . 14  |-  ( ( f  o F  .+  g )  e.  {
x  |  ps }  <->  ze )
41 oveq1 6027 . . . . . . . . . . . . . . 15  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( f  o F  .+  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F 
.+  g ) )
4241eleq1d 2453 . . . . . . . . . . . . . 14  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
f  o F  .+  g )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .+  g
)  e.  { x  |  ps } ) )
4340, 42syl5bbr 251 . . . . . . . . . . . . 13  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( ze  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .+  g
)  e.  { x  |  ps } ) )
4437, 43imbi12d 312 . . . . . . . . . . . 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 } ) ) )  o F  .+  g )  e.  {
x  |  ps }
) ) )
45 vex 2902 . . . . . . . . . . . . . . . . 17  |-  g  e. 
_V
46 pf1ind.wd . . . . . . . . . . . . . . . . 17  |-  ( x  =  g  ->  ( ps 
<->  et ) )
4745, 46elab 3025 . . . . . . . . . . . . . . . 16  |-  ( g  e.  { x  |  ps }  <->  et )
48 eleq1 2447 . . . . . . . . . . . . . . . 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 251 . . . . . . . . . . . . . . 15  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( et  <->  ( b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } ) )
5049anbi2d 685 . . . . . . . . . . . . . 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 686 . . . . . . . . . . . . 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 6028 . . . . . . . . . . . . . 14  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  o F  .+  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F 
.+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) ) )
5352eleq1d 2453 . . . . . . . . . . . . 13  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .+  g
)  e.  { x  |  ps }  <->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  o F  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
5451, 53imbi12d 312 . . . . . . . . . . . 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 } ) ) )  o F 
.+  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 } ) ) )  o F 
.+  ( 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 425 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) )  ->  ( ph  ->  ze ) )
5756an4s 800 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  Q  /\  g  e.  Q
)  /\  ( ta  /\  et ) )  -> 
( ph  ->  ze )
)
5857expimpd 587 . . . . . . . . . . . 12  |-  ( ( f  e.  Q  /\  g  e.  Q )  ->  ( ( ( ta 
/\  et )  /\  ph )  ->  ze )
)
5944, 54, 58vtocl2ga 2962 . . . . . . . . . . 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 }
) ) )  o F  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
6029, 30, 59syl2an 464 . . . . . . . . . 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 }
) ) )  o F  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
6160exp3acom23 1378 . . . . . . . . 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 } ) ) )  o F  .+  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e.  { x  |  ps } ) ) )
6261impcom 420 . . . . . . . 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 } ) ) )  o F  .+  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
6326, 3mpff 19829 . . . . . . . . . . . 12  |-  ( a  e.  ran  ( 1o eval  R )  ->  a : ( B  ^m  1o ) --> B )
6463ad2antrl 709 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  a : ( B  ^m  1o ) --> B )
65 ffn 5531 . . . . . . . . . . 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 19829 . . . . . . . . . . . 12  |-  ( b  e.  ran  ( 1o eval  R )  ->  b : ( B  ^m  1o ) --> B )
6867ad2antll 710 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  b : ( B  ^m  1o ) --> B )
69 ffn 5531 . . . . . . . . . . 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 2387 . . . . . . . . . . . 12  |-  ( w  e.  B  |->  ( 1o 
X.  { w }
) )  =  ( w  e.  B  |->  ( 1o  X.  { w } ) )
722, 5, 6, 71mapsnf1o3 6998 . . . . . . . . . . 11  |-  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) : B -1-1-onto-> ( B  ^m  1o )
73 f1of 5614 . . . . . . . . . . 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 6045 . . . . . . . . . . 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 3493 . . . . . . . . . 10  |-  ( ( B  ^m  1o )  i^i  ( B  ^m  1o ) )  =  ( B  ^m  1o )
7966, 70, 74, 76, 76, 77, 78ofco 6263 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( a  o F 
.+  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  o F  .+  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) ) )
8079eleq1d 2453 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  o F  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .+  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
8162, 80sylibrd 226 . . . . . . 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  o F 
.+  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
8281expimpd 587 . . . . . 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  o F  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
8327, 82syl5bi 209 . . . . 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  o F  .+  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
8483imp 419 . . . 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  o F  .+  b
)  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
85 ovex 6045 . . . . . . . . . . . . . . 15  |-  ( f  o F  .x.  g
)  e.  _V
86 pf1ind.wf . . . . . . . . . . . . . . 15  |-  ( x  =  ( f  o F  .x.  g )  ->  ( ps  <->  si )
)
8785, 86elab 3025 . . . . . . . . . . . . . 14  |-  ( ( f  o F  .x.  g )  e.  {
x  |  ps }  <->  si )
88 oveq1 6027 . . . . . . . . . . . . . . 15  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( f  o F  .x.  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F 
.x.  g ) )
8988eleq1d 2453 . . . . . . . . . . . . . 14  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
f  o F  .x.  g )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .x.  g
)  e.  { x  |  ps } ) )
9087, 89syl5bbr 251 . . . . . . . . . . . . 13  |-  ( f  =  ( a  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( si  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .x.  g
)  e.  { x  |  ps } ) )
9137, 90imbi12d 312 . . . . . . . . . . . 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 } ) ) )  o F  .x.  g )  e.  {
x  |  ps }
) ) )
92 oveq2 6028 . . . . . . . . . . . . . 14  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  o F  .x.  g )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F 
.x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) ) ) )
9392eleq1d 2453 . . . . . . . . . . . . 13  |-  ( g  =  ( b  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  ->  ( (
( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .x.  g
)  e.  { x  |  ps }  <->  ( (
a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  o F  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
9451, 93imbi12d 312 . . . . . . . . . . . 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 } ) ) )  o F 
.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 } ) ) )  o F 
.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 425 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  Q  /\  ta )  /\  (
g  e.  Q  /\  et ) )  ->  ( ph  ->  si ) )
9796an4s 800 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  Q  /\  g  e.  Q
)  /\  ( ta  /\  et ) )  -> 
( ph  ->  si )
)
9897expimpd 587 . . . . . . . . . . . 12  |-  ( ( f  e.  Q  /\  g  e.  Q )  ->  ( ( ( ta 
/\  et )  /\  ph )  ->  si )
)
9991, 94, 98vtocl2ga 2962 . . . . . . . . . . 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 }
) ) )  o F  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
10029, 30, 99syl2an 464 . . . . . . . . . 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 }
) ) )  o F  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e. 
{ x  |  ps } ) )
101100exp3acom23 1378 . . . . . . . . 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 } ) ) )  o F  .x.  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )  e.  { x  |  ps } ) ) )
102101impcom 420 . . . . . . . 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 } ) ) )  o F  .x.  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
10366, 70, 74, 76, 76, 77, 78ofco 6263 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( a  o F 
.x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  o F  .x.  ( b  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) ) ) )
104103eleq1d 2453 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  ran  ( 1o eval  R
)  /\  b  e.  ran  ( 1o eval  R ) ) )  ->  (
( ( a  o F  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  o F  .x.  (
b  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) ) )  e.  { x  |  ps } ) )
105102, 104sylibrd 226 . . . . . . 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  o F 
.x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
106105expimpd 587 . . . . . 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  o F  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
10727, 106syl5bi 209 . . . . 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  o F  .x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }
) )
108107imp 419 . . . 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  o F  .x.  b
)  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
109 coeq1 4970 . . . . 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 2453 . . . 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 4970 . . . . 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 2453 . . . 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 4970 . . . . 5  |-  ( y  =  a  ->  (
y  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  =  ( a  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
114113eleq1d 2453 . . . 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 4970 . . . . 5  |-  ( y  =  b  ->  (
y  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  =  ( b  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
116115eleq1d 2453 . . . 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 4970 . . . . 5  |-  ( y  =  ( a  o F  .+  b )  ->  ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  o F  .+  b )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
118117eleq1d 2453 . . . 4  |-  ( y  =  ( a  o F  .+  b )  ->  ( ( y  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  o F 
.+  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
119 coeq1 4970 . . . . 5  |-  ( y  =  ( a  o F  .x.  b )  ->  ( y  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  =  ( ( a  o F  .x.  b )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) ) )
120119eleq1d 2453 . . . 4  |-  ( y  =  ( a  o F  .x.  b )  ->  ( ( y  o.  ( w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  {
x  |  ps }  <->  ( ( a  o F 
.x.  b )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
121 coeq1 4970 . . . . 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 2453 . . . 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 19836 . . . . . . . . 9  |-  ( A  e.  Q  ->  R  e.  CRing )
12416, 123syl 16 . . . . . . . 8  |-  ( ph  ->  R  e.  CRing )
125124adantr 452 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  R  e.  CRing )
126 1on 6667 . . . . . . . . . . . 12  |-  1o  e.  On
127 eqid 2387 . . . . . . . . . . . . 13  |-  ( 1o mPoly  R )  =  ( 1o mPoly  R )
128127mplassa 16444 . . . . . . . . . . . 12  |-  ( ( 1o  e.  On  /\  R  e.  CRing )  -> 
( 1o mPoly  R )  e. AssAlg )
129126, 124, 128sylancr 645 . . . . . . . . . . 11  |-  ( ph  ->  ( 1o mPoly  R )  e. AssAlg )
130 eqid 2387 . . . . . . . . . . . . 13  |-  (Poly1 `  R
)  =  (Poly1 `  R
)
131 eqid 2387 . . . . . . . . . . . . 13  |-  (algSc `  (Poly1 `  R ) )  =  (algSc `  (Poly1 `  R
) )
132130, 131ply1ascl 16578 . . . . . . . . . . . 12  |-  (algSc `  (Poly1 `  R ) )  =  (algSc `  ( 1o mPoly  R ) )
133 eqid 2387 . . . . . . . . . . . 12  |-  (Scalar `  ( 1o mPoly  R ) )  =  (Scalar `  ( 1o mPoly  R ) )
134132, 133asclrhm 16327 . . . . . . . . . . 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 16435 . . . . . . . . . . 11  |-  ( ph  ->  R  =  (Scalar `  ( 1o mPoly  R ) ) )
138137oveq1d 6035 . . . . . . . . . 10  |-  ( ph  ->  ( R RingHom  ( 1o mPoly  R ) )  =  ( (Scalar `  ( 1o mPoly  R ) ) RingHom  ( 1o mPoly  R ) ) )
139135, 138eleqtrrd 2464 . . . . . . . . 9  |-  ( ph  ->  (algSc `  (Poly1 `  R
) )  e.  ( R RingHom  ( 1o mPoly  R
) ) )
140 eqid 2387 . . . . . . . . . 10  |-  ( Base `  ( 1o mPoly  R )
)  =  ( Base `  ( 1o mPoly  R )
)
1413, 140rhmf 15754 . . . . . . . . 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 5809 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  (
(algSc `  (Poly1 `  R
) ) `  a
)  e.  ( Base `  ( 1o mPoly  R )
) )
144 eqid 2387 . . . . . . . 8  |-  (eval1 `  R
)  =  (eval1 `  R
)
145144, 24, 3, 127, 140evl1val 19815 . . . . . . 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 643 . . . . . 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 19817 . . . . . . 7  |-  ( ( R  e.  CRing  /\  a  e.  B )  ->  (
(eval1 `
 R ) `  ( (algSc `  (Poly1 `  R
) ) `  a
) )  =  ( B  X.  { a } ) )
148124, 147sylan 458 . . . . . 6  |-  ( (
ph  /\  a  e.  B )  ->  (
(eval1 `
 R ) `  ( (algSc `  (Poly1 `  R
) ) `  a
) )  =  ( B  X.  { a } ) )
1493ressid 13451 . . . . . . . . . . . . . 14  |-  ( R  e.  CRing  ->  ( Rs  B
)  =  R )
150125, 149syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  B )  ->  ( Rs  B )  =  R )
151150oveq2d 6036 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  B )  ->  ( 1o mPoly  ( Rs  B ) )  =  ( 1o mPoly  R )
)
152151fveq2d 5672 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  B )  ->  (algSc `  ( 1o mPoly  ( Rs  B
) ) )  =  (algSc `  ( 1o mPoly  R ) ) )
153152, 132syl6eqr 2437 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  B )  ->  (algSc `  ( 1o mPoly  ( Rs  B
) ) )  =  (algSc `  (Poly1 `  R
) ) )
154153fveq1d 5670 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  (
(algSc `  ( 1o mPoly  ( Rs  B ) ) ) `
 a )  =  ( (algSc `  (Poly1 `  R ) ) `  a ) )
155154fveq2d 5672 . . . . . . . 8  |-  ( (
ph  /\  a  e.  B )  ->  (
( 1o eval  R ) `  ( (algSc `  ( 1o mPoly  ( Rs  B ) ) ) `
 a ) )  =  ( ( 1o eval  R ) `  (
(algSc `  (Poly1 `  R
) ) `  a
) ) )
156 eqid 2387 . . . . . . . . 9  |-  ( 1o mPoly 
( Rs  B ) )  =  ( 1o mPoly  ( Rs  B
) )
157 eqid 2387 . . . . . . . . 9  |-  ( Rs  B )  =  ( Rs  B )
158 eqid 2387 . . . . . . . . 9  |-  (algSc `  ( 1o mPoly  ( Rs  B
) ) )  =  (algSc `  ( 1o mPoly  ( Rs  B ) ) )
159126a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  1o  e.  On )
160 crngrng 15601 . . . . . . . . . . 11  |-  ( R  e.  CRing  ->  R  e.  Ring )
1613subrgid 15797 . . . . . . . . . . 11  |-  ( R  e.  Ring  ->  B  e.  (SubRing `  R )
)
162124, 160, 1613syl 19 . . . . . . . . . 10  |-  ( ph  ->  B  e.  (SubRing `  R
) )
163162adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  B  e.  (SubRing `  R )
)
164 simpr 448 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  B )  ->  a  e.  B )
16525, 156, 157, 3, 158, 159, 125, 163, 164evlssca 19810 . . . . . . . 8  |-  ( (
ph  /\  a  e.  B )  ->  (
( 1o eval  R ) `  ( (algSc `  ( 1o mPoly  ( Rs  B ) ) ) `
 a ) )  =  ( ( B  ^m  1o )  X. 
{ a } ) )
166155, 165eqtr3d 2421 . . . . . . 7  |-  ( (
ph  /\  a  e.  B )  ->  (
( 1o eval  R ) `  ( (algSc `  (Poly1 `  R ) ) `  a ) )  =  ( ( B  ^m  1o )  X.  { a } ) )
167166coeq1d 4974 . . . . . 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 2427 . . . . 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 4346 . . . . . . . . . 10  |-  { f }  e.  _V
1715, 170xpex 4930 . . . . . . . . 9  |-  ( B  X.  { f } )  e.  _V
172 pf1ind.wa . . . . . . . . 9  |-  ( x  =  ( B  X.  { f } )  ->  ( ps  <->  ch )
)
173171, 172elab 3025 . . . . . . . 8  |-  ( ( B  X.  { f } )  e.  {
x  |  ps }  <->  ch )
174169, 173sylibr 204 . . . . . . 7  |-  ( (
ph  /\  f  e.  B )  ->  ( B  X.  { f } )  e.  { x  |  ps } )
175174ralrimiva 2732 . . . . . 6  |-  ( ph  ->  A. f  e.  B  ( B  X.  { f } )  e.  {
x  |  ps }
)
176 sneq 3768 . . . . . . . . 9  |-  ( f  =  a  ->  { f }  =  { a } )
177176xpeq2d 4842 . . . . . . . 8  |-  ( f  =  a  ->  ( B  X.  { f } )  =  ( B  X.  { a } ) )
178177eleq1d 2453 . . . . . . 7  |-  ( f  =  a  ->  (
( B  X.  {
f } )  e. 
{ x  |  ps } 
<->  ( B  X.  {
a } )  e. 
{ x  |  ps } ) )
179178rspccva 2994 . . . . . 6  |-  ( ( A. f  e.  B  ( B  X.  { f } )  e.  {
x  |  ps }  /\  a  e.  B
)  ->  ( B  X.  { a } )  e.  { x  |  ps } )
180175, 179sylan 458 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  ( B  X.  { a } )  e.  { x  |  ps } )
181168, 180eqeltrrd 2462 . . . 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 5128 . . . . . . . . . 10  |-  ( B  e.  _V  ->  (  _I  |`  B )  e. 
_V )
1845, 183ax-mp 8 . . . . . . . . 9  |-  (  _I  |`  B )  e.  _V
185 pf1ind.wb . . . . . . . . 9  |-  ( x  =  (  _I  |`  B )  ->  ( ps  <->  th )
)
186184, 185elab 3025 . . . . . . . 8  |-  ( (  _I  |`  B )  e.  { x  |  ps } 
<->  th )
187182, 186sylibr 204 . . . . . . 7  |-  ( ph  ->  (  _I  |`  B )  e.  { x  |  ps } )
18813, 187eqeltrd 2461 . . . . . 6  |-  ( ph  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  (/) ) )  o.  (
w  e.  B  |->  ( 1o  X.  { w } ) ) )  e.  { x  |  ps } )
189 el1o 6679 . . . . . . . . . 10  |-  ( a  e.  1o  <->  a  =  (/) )
190 fveq2 5668 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( b `
 a )  =  ( b `  (/) ) )
191189, 190sylbi 188 . . . . . . . . 9  |-  ( a  e.  1o  ->  (
b `  a )  =  ( b `  (/) ) )
192191mpteq2dv 4237 . . . . . . . 8  |-  ( a  e.  1o  ->  (
b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  =  ( b  e.  ( B  ^m  1o )  |->  ( b `
 (/) ) ) )
193192coeq1d 4974 . . . . . . 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 2453 . . . . . 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 214 . . . . 5  |-  ( ph  ->  ( a  e.  1o  ->  ( ( b  e.  ( B  ^m  1o )  |->  ( b `  a ) )  o.  ( w  e.  B  |->  ( 1o  X.  {
w } ) ) )  e.  { x  |  ps } ) )
196195imp 419 . . . 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 19839 . . . . 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 19832 . . 3  |-  ( ph  ->  ( ( A  o.  ( b  e.  ( B  ^m  1o ) 
|->  ( b `  (/) ) ) )  o.  ( w  e.  B  |->  ( 1o 
X.  { w }
) ) )  e. 
{ x  |  ps } )
20021, 199eqeltrrd 2462 . 2  |-  ( ph  ->  A  e.  { x  |  ps } )
201 pf1ind.wg . . . 4  |-  ( x  =  A  ->  ( ps 
<->  rh ) )
202201elabg 3026 . . 3  |-  ( A  e.  Q  ->  ( A  e.  { x  |  ps }  <->  rh )
)
20316, 202syl 16 . 2  |-  ( ph  ->  ( A  e.  {
x  |  ps }  <->  rh ) )
204200, 203mpbid 202 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   {cab 2373   A.wral 2649   _Vcvv 2899   (/)c0 3571   {csn 3757    e. cmpt 4207    _I cid 4434   Oncon0 4522    X. cxp 4816   `'ccnv 4817   ran crn 4819    |` cres 4820    o. ccom 4822    Fn wfn 5389   -->wf 5390   -1-1-onto->wf1o 5393   ` cfv 5394  (class class class)co 6020    o Fcof 6242   1oc1o 6653    ^m cmap 6954   Basecbs 13396   ↾s cress 13397   +g cplusg 13456   .rcmulr 13457  Scalarcsca 13459   Ringcrg 15587   CRingccrg 15588   RingHom crh 15744  SubRingcsubrg 15791  AssAlgcasa 16296  algSccascl 16298   mPoly cmpl 16335   evalSub ces 16336   eval cevl 16337  Poly1cpl1 16498  eval1ce1 16500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-inf2 7529  ax-cnex 8979  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-int 3993  df-iun 4037  df-iin 4038  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-se 4483  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-isom 5403  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-of 6244  df-ofr 6245  df-1st 6288  df-2nd 6289  df-riota 6485  df-recs 6569  df-rdg 6604  df-1o 6660  df-2o 6661  df-oadd 6664  df-er 6841  df-map 6956  df-pm 6957  df-ixp 7000  df-en 7046  df-dom 7047  df-sdom 7048  df-fin 7049  df-sup 7381  df-oi 7412  df-card 7759  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-nn 9933  df-2 9990  df-3 9991  df-4 9992  df-5 9993  df-6 9994  df-7 9995  df-8 9996  df-9 9997  df-10 9998  df-n0 10154  df-z 10215  df-dec 10315  df-uz 10421  df-fz 10976  df-fzo 11066  df-seq 11251  df-hash 11546  df-struct 13398  df-ndx 13399  df-slot 13400  df-base 13401  df-sets 13402  df-ress 13403  df-plusg 13469  df-mulr 13470  df-sca 13472  df-vsca 13473  df-tset 13475  df-ple 13476  df-ds 13478  df-hom 13480  df-cco 13481  df-prds 13598  df-pws 13600  df-0g 13654  df-gsum 13655  df-mre 13738  df-mrc 13739  df-acs 13741  df-mnd 14617  df-mhm 14665  df-submnd 14666  df-grp 14739  df-minusg 14740  df-sbg 14741  df-mulg 14742  df-subg 14868  df-ghm 14931  df-cntz 15043  df-cmn 15341  df-abl 15342  df-mgp 15576  df-rng 15590  df-cring 15591  df-ur 15592  df-rnghom 15746  df-subrg 15793  df-lmod 15879  df-lss 15936  df-lsp 15975  df-assa 16299  df-asp 16300  df-ascl 16301  df-psr 16344  df-mvr 16345  df-mpl 16346  df-evls 16347  df-evl 16348  df-opsr 16352  df-psr1 16503  df-ply1 16505  df-evl1 16507
  Copyright terms: Public domain W3C validator