This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pf1ind

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)

Ref Expression
Hypotheses 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 pf1ind 
|- ( ph -> rh )

Proof

Step Hyp Ref Expression
1 pf1ind.cb 
 |-  B = ( Base ` R )
2 pf1ind.cp 
 |-  .+ = ( +g ` R )
3 pf1ind.ct 
 |-  .x. = ( .r ` R )
4 pf1ind.cq 
 |-  Q = ran ( eval1 ` R )
5 pf1ind.ad 
 |-  ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze )
6 pf1ind.mu 
 |-  ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si )
7 pf1ind.wa 
 |-  ( x = ( B X. { f } ) -> ( ps <-> ch ) )
8 pf1ind.wb 
 |-  ( x = ( _I |` B ) -> ( ps <-> th ) )
9 pf1ind.wc 
 |-  ( x = f -> ( ps <-> ta ) )
10 pf1ind.wd 
 |-  ( x = g -> ( ps <-> et ) )
11 pf1ind.we 
 |-  ( x = ( f oF .+ g ) -> ( ps <-> ze ) )
12 pf1ind.wf 
 |-  ( x = ( f oF .x. g ) -> ( ps <-> si ) )
13 pf1ind.wg 
 |-  ( x = A -> ( ps <-> rh ) )
14 pf1ind.co 
 |-  ( ( ph /\ f e. B ) -> ch )
15 pf1ind.pr 
 |-  ( ph -> th )
16 pf1ind.a 
 |-  ( ph -> A e. Q )
17 coass 
 |-  ( ( 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 } ) ) ) )
18 df1o2 
 |-  1o = { (/) }
19 1 fvexi 
 |-  B e. _V
20 0ex 
 |-  (/) e. _V
21 eqid 
 |-  ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) = ( b e. ( B ^m 1o ) |-> ( b ` (/) ) )
22 18 19 20 21 mapsncnv 
 |-  `' ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) = ( w e. B |-> ( 1o X. { w } ) )
23 22 coeq2i 
 |-  ( ( 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 } ) ) )
24 18 19 20 21 mapsnf1o2 
 |-  ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) : ( B ^m 1o ) -1-1-onto-> B
25 f1ococnv2 
 |-  ( ( 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 ) )
26 24 25 mp1i 
 |-  ( ph -> ( ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) o. `' ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) ) = ( _I |` B ) )
27 23 26 eqtr3id 
 |-  ( ph -> ( ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) = ( _I |` B ) )
28 27 coeq2d 
 |-  ( ph -> ( A o. ( ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) ) = ( A o. ( _I |` B ) ) )
29 17 28 eqtrid 
 |-  ( ph -> ( ( A o. ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) = ( A o. ( _I |` B ) ) )
30 4 1 pf1f 
 |-  ( A e. Q -> A : B --> B )
31 fcoi1 
 |-  ( A : B --> B -> ( A o. ( _I |` B ) ) = A )
32 16 30 31 3syl 
 |-  ( ph -> ( A o. ( _I |` B ) ) = A )
33 29 32 eqtrd 
 |-  ( ph -> ( ( A o. ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) = A )
34 eqid 
 |-  ( 1o eval R ) = ( 1o eval R )
35 34 1 evlval 
 |-  ( 1o eval R ) = ( ( 1o evalSub R ) ` B )
36 35 rneqi 
 |-  ran ( 1o eval R ) = ran ( ( 1o evalSub R ) ` B )
37 an4 
 |-  ( ( ( 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 } ) ) )
38 eqid 
 |-  ran ( 1o eval R ) = ran ( 1o eval R )
39 4 1 38 mpfpf1 
 |-  ( a e. ran ( 1o eval R ) -> ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) e. Q )
40 4 1 38 mpfpf1 
 |-  ( b e. ran ( 1o eval R ) -> ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) e. Q )
41 vex 
 |-  f e. _V
42 41 9 elab 
 |-  ( f e. { x | ps } <-> ta )
43 eleq1 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( f e. { x | ps } <-> ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
44 42 43 bitr3id 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( ta <-> ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
45 44 anbi1d 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( ( ta /\ et ) <-> ( ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } /\ et ) ) )
46 45 anbi1d 
 |-  ( 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 ) ) )
47 ovex 
 |-  ( f oF .+ g ) e. _V
48 47 11 elab 
 |-  ( ( f oF .+ g ) e. { x | ps } <-> ze )
49 oveq1 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( f oF .+ g ) = ( ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) oF .+ g ) )
50 49 eleq1d 
 |-  ( 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 } ) )
51 48 50 bitr3id 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( ze <-> ( ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) oF .+ g ) e. { x | ps } ) )
52 46 51 imbi12d 
 |-  ( 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 } ) ) )
53 vex 
 |-  g e. _V
54 53 10 elab 
 |-  ( g e. { x | ps } <-> et )
55 eleq1 
 |-  ( g = ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( g e. { x | ps } <-> ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
56 54 55 bitr3id 
 |-  ( g = ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( et <-> ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
57 56 anbi2d 
 |-  ( 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 } ) ) )
58 57 anbi1d 
 |-  ( 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 ) ) )
59 oveq2 
 |-  ( 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 } ) ) ) ) )
60 59 eleq1d 
 |-  ( 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 } ) )
61 58 60 imbi12d 
 |-  ( 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 } ) ) )
62 5 expcom 
 |-  ( ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) -> ( ph -> ze ) )
63 62 an4s 
 |-  ( ( ( f e. Q /\ g e. Q ) /\ ( ta /\ et ) ) -> ( ph -> ze ) )
64 63 expimpd 
 |-  ( ( f e. Q /\ g e. Q ) -> ( ( ( ta /\ et ) /\ ph ) -> ze ) )
65 52 61 64 vtocl2ga 
 |-  ( ( ( 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 } ) )
66 39 40 65 syl2an 
 |-  ( ( 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 } ) )
67 66 expcomd 
 |-  ( ( 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 } ) ) )
68 67 impcom 
 |-  ( ( 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 } ) )
69 36 1 mpff 
 |-  ( a e. ran ( 1o eval R ) -> a : ( B ^m 1o ) --> B )
70 69 ad2antrl 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> a : ( B ^m 1o ) --> B )
71 70 ffnd 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> a Fn ( B ^m 1o ) )
72 36 1 mpff 
 |-  ( b e. ran ( 1o eval R ) -> b : ( B ^m 1o ) --> B )
73 72 ad2antll 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> b : ( B ^m 1o ) --> B )
74 73 ffnd 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> b Fn ( B ^m 1o ) )
75 eqid 
 |-  ( w e. B |-> ( 1o X. { w } ) ) = ( w e. B |-> ( 1o X. { w } ) )
76 18 19 20 75 mapsnf1o3 
 |-  ( w e. B |-> ( 1o X. { w } ) ) : B -1-1-onto-> ( B ^m 1o )
77 f1of 
 |-  ( ( w e. B |-> ( 1o X. { w } ) ) : B -1-1-onto-> ( B ^m 1o ) -> ( w e. B |-> ( 1o X. { w } ) ) : B --> ( B ^m 1o ) )
78 76 77 mp1i 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> ( w e. B |-> ( 1o X. { w } ) ) : B --> ( B ^m 1o ) )
79 ovexd 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> ( B ^m 1o ) e. _V )
80 19 a1i 
 |-  ( ( ph /\ ( a e. ran ( 1o eval R ) /\ b e. ran ( 1o eval R ) ) ) -> B e. _V )
81 inidm 
 |-  ( ( B ^m 1o ) i^i ( B ^m 1o ) ) = ( B ^m 1o )
82 71 74 78 79 79 80 81 ofco 
 |-  ( ( 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 } ) ) ) ) )
83 82 eleq1d 
 |-  ( ( 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 } ) )
84 68 83 sylibrd 
 |-  ( ( 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 } ) )
85 84 expimpd 
 |-  ( 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 } ) )
86 37 85 biimtrid 
 |-  ( 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 } ) )
87 86 imp 
 |-  ( ( 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 } )
88 ovex 
 |-  ( f oF .x. g ) e. _V
89 88 12 elab 
 |-  ( ( f oF .x. g ) e. { x | ps } <-> si )
90 oveq1 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( f oF .x. g ) = ( ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) oF .x. g ) )
91 90 eleq1d 
 |-  ( 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 } ) )
92 89 91 bitr3id 
 |-  ( f = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) -> ( si <-> ( ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) oF .x. g ) e. { x | ps } ) )
93 46 92 imbi12d 
 |-  ( 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 } ) ) )
94 oveq2 
 |-  ( 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 } ) ) ) ) )
95 94 eleq1d 
 |-  ( 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 } ) )
96 58 95 imbi12d 
 |-  ( 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 } ) ) )
97 6 expcom 
 |-  ( ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) -> ( ph -> si ) )
98 97 an4s 
 |-  ( ( ( f e. Q /\ g e. Q ) /\ ( ta /\ et ) ) -> ( ph -> si ) )
99 98 expimpd 
 |-  ( ( f e. Q /\ g e. Q ) -> ( ( ( ta /\ et ) /\ ph ) -> si ) )
100 93 96 99 vtocl2ga 
 |-  ( ( ( 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 } ) )
101 39 40 100 syl2an 
 |-  ( ( 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 } ) )
102 101 expcomd 
 |-  ( ( 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 } ) ) )
103 102 impcom 
 |-  ( ( 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 } ) )
104 71 74 78 79 79 80 81 ofco 
 |-  ( ( 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 } ) ) ) ) )
105 104 eleq1d 
 |-  ( ( 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 } ) )
106 103 105 sylibrd 
 |-  ( ( 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 } ) )
107 106 expimpd 
 |-  ( 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 } ) )
108 37 107 biimtrid 
 |-  ( 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 108 imp 
 |-  ( ( 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 } )
110 coeq1 
 |-  ( 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 } ) ) ) )
111 110 eleq1d 
 |-  ( 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 } ) )
112 coeq1 
 |-  ( 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 } ) ) ) )
113 112 eleq1d 
 |-  ( 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 } ) )
114 coeq1 
 |-  ( y = a -> ( y o. ( w e. B |-> ( 1o X. { w } ) ) ) = ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) )
115 114 eleq1d 
 |-  ( y = a -> ( ( y o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } <-> ( a o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
116 coeq1 
 |-  ( y = b -> ( y o. ( w e. B |-> ( 1o X. { w } ) ) ) = ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) )
117 116 eleq1d 
 |-  ( y = b -> ( ( y o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } <-> ( b o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
118 coeq1 
 |-  ( y = ( a oF .+ b ) -> ( y o. ( w e. B |-> ( 1o X. { w } ) ) ) = ( ( a oF .+ b ) o. ( w e. B |-> ( 1o X. { w } ) ) ) )
119 118 eleq1d 
 |-  ( 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 } ) )
120 coeq1 
 |-  ( y = ( a oF .x. b ) -> ( y o. ( w e. B |-> ( 1o X. { w } ) ) ) = ( ( a oF .x. b ) o. ( w e. B |-> ( 1o X. { w } ) ) ) )
121 120 eleq1d 
 |-  ( 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 } ) )
122 coeq1 
 |-  ( 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 } ) ) ) )
123 122 eleq1d 
 |-  ( 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 } ) )
124 4 pf1rcl 
 |-  ( A e. Q -> R e. CRing )
125 16 124 syl 
 |-  ( ph -> R e. CRing )
126 125 adantr 
 |-  ( ( ph /\ a e. B ) -> R e. CRing )
127 1on 
 |-  1o e. On
128 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
129 128 mplassa 
 |-  ( ( 1o e. On /\ R e. CRing ) -> ( 1o mPoly R ) e. AssAlg )
130 127 125 129 sylancr 
 |-  ( ph -> ( 1o mPoly R ) e. AssAlg )
131 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
132 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
133 131 132 ply1ascl 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( 1o mPoly R ) )
134 eqid 
 |-  ( Scalar ` ( 1o mPoly R ) ) = ( Scalar ` ( 1o mPoly R ) )
135 133 134 asclrhm 
 |-  ( ( 1o mPoly R ) e. AssAlg -> ( algSc ` ( Poly1 ` R ) ) e. ( ( Scalar ` ( 1o mPoly R ) ) RingHom ( 1o mPoly R ) ) )
136 130 135 syl 
 |-  ( ph -> ( algSc ` ( Poly1 ` R ) ) e. ( ( Scalar ` ( 1o mPoly R ) ) RingHom ( 1o mPoly R ) ) )
137 127 a1i 
 |-  ( ph -> 1o e. On )
138 128 137 125 mplsca 
 |-  ( ph -> R = ( Scalar ` ( 1o mPoly R ) ) )
139 138 oveq1d 
 |-  ( ph -> ( R RingHom ( 1o mPoly R ) ) = ( ( Scalar ` ( 1o mPoly R ) ) RingHom ( 1o mPoly R ) ) )
140 136 139 eleqtrrd 
 |-  ( ph -> ( algSc ` ( Poly1 ` R ) ) e. ( R RingHom ( 1o mPoly R ) ) )
141 eqid 
 |-  ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
142 1 141 rhmf 
 |-  ( ( algSc ` ( Poly1 ` R ) ) e. ( R RingHom ( 1o mPoly R ) ) -> ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( 1o mPoly R ) ) )
143 140 142 syl 
 |-  ( ph -> ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( 1o mPoly R ) ) )
144 143 ffvelcdmda 
 |-  ( ( ph /\ a e. B ) -> ( ( algSc ` ( Poly1 ` R ) ) ` a ) e. ( Base ` ( 1o mPoly R ) ) )
145 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
146 145 34 1 128 141 evl1val 
 |-  ( ( 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 } ) ) ) )
147 126 144 146 syl2anc 
 |-  ( ( ph /\ a e. B ) -> ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` a ) ) = ( ( ( 1o eval R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` a ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) )
148 145 131 1 132 evl1sca 
 |-  ( ( R e. CRing /\ a e. B ) -> ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` a ) ) = ( B X. { a } ) )
149 125 148 sylan 
 |-  ( ( ph /\ a e. B ) -> ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` a ) ) = ( B X. { a } ) )
150 1 ressid 
 |-  ( R e. CRing -> ( R |`s B ) = R )
151 126 150 syl 
 |-  ( ( ph /\ a e. B ) -> ( R |`s B ) = R )
152 151 oveq2d 
 |-  ( ( ph /\ a e. B ) -> ( 1o mPoly ( R |`s B ) ) = ( 1o mPoly R ) )
153 152 fveq2d 
 |-  ( ( ph /\ a e. B ) -> ( algSc ` ( 1o mPoly ( R |`s B ) ) ) = ( algSc ` ( 1o mPoly R ) ) )
154 153 133 eqtr4di 
 |-  ( ( ph /\ a e. B ) -> ( algSc ` ( 1o mPoly ( R |`s B ) ) ) = ( algSc ` ( Poly1 ` R ) ) )
155 154 fveq1d 
 |-  ( ( ph /\ a e. B ) -> ( ( algSc ` ( 1o mPoly ( R |`s B ) ) ) ` a ) = ( ( algSc ` ( Poly1 ` R ) ) ` a ) )
156 155 fveq2d 
 |-  ( ( ph /\ a e. B ) -> ( ( 1o eval R ) ` ( ( algSc ` ( 1o mPoly ( R |`s B ) ) ) ` a ) ) = ( ( 1o eval R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` a ) ) )
157 eqid 
 |-  ( 1o mPoly ( R |`s B ) ) = ( 1o mPoly ( R |`s B ) )
158 eqid 
 |-  ( R |`s B ) = ( R |`s B )
159 eqid 
 |-  ( algSc ` ( 1o mPoly ( R |`s B ) ) ) = ( algSc ` ( 1o mPoly ( R |`s B ) ) )
160 127 a1i 
 |-  ( ( ph /\ a e. B ) -> 1o e. On )
161 crngring 
 |-  ( R e. CRing -> R e. Ring )
162 1 subrgid 
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
163 125 161 162 3syl 
 |-  ( ph -> B e. ( SubRing ` R ) )
164 163 adantr 
 |-  ( ( ph /\ a e. B ) -> B e. ( SubRing ` R ) )
165 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
166 35 157 158 1 159 160 126 164 165 evlssca 
 |-  ( ( ph /\ a e. B ) -> ( ( 1o eval R ) ` ( ( algSc ` ( 1o mPoly ( R |`s B ) ) ) ` a ) ) = ( ( B ^m 1o ) X. { a } ) )
167 156 166 eqtr3d 
 |-  ( ( ph /\ a e. B ) -> ( ( 1o eval R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` a ) ) = ( ( B ^m 1o ) X. { a } ) )
168 167 coeq1d 
 |-  ( ( 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 } ) ) ) )
169 147 149 168 3eqtr3d 
 |-  ( ( ph /\ a e. B ) -> ( B X. { a } ) = ( ( ( B ^m 1o ) X. { a } ) o. ( w e. B |-> ( 1o X. { w } ) ) ) )
170 vsnex 
 |-  { f } e. _V
171 19 170 xpex 
 |-  ( B X. { f } ) e. _V
172 171 7 elab 
 |-  ( ( B X. { f } ) e. { x | ps } <-> ch )
173 14 172 sylibr 
 |-  ( ( ph /\ f e. B ) -> ( B X. { f } ) e. { x | ps } )
174 173 ralrimiva 
 |-  ( ph -> A. f e. B ( B X. { f } ) e. { x | ps } )
175 sneq 
 |-  ( f = a -> { f } = { a } )
176 175 xpeq2d 
 |-  ( f = a -> ( B X. { f } ) = ( B X. { a } ) )
177 176 eleq1d 
 |-  ( f = a -> ( ( B X. { f } ) e. { x | ps } <-> ( B X. { a } ) e. { x | ps } ) )
178 177 rspccva 
 |-  ( ( A. f e. B ( B X. { f } ) e. { x | ps } /\ a e. B ) -> ( B X. { a } ) e. { x | ps } )
179 174 178 sylan 
 |-  ( ( ph /\ a e. B ) -> ( B X. { a } ) e. { x | ps } )
180 169 179 eqeltrrd 
 |-  ( ( ph /\ a e. B ) -> ( ( ( B ^m 1o ) X. { a } ) o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } )
181 resiexg 
 |-  ( B e. _V -> ( _I |` B ) e. _V )
182 19 181 ax-mp 
 |-  ( _I |` B ) e. _V
183 182 8 elab 
 |-  ( ( _I |` B ) e. { x | ps } <-> th )
184 15 183 sylibr 
 |-  ( ph -> ( _I |` B ) e. { x | ps } )
185 27 184 eqeltrd 
 |-  ( ph -> ( ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } )
186 el1o 
 |-  ( a e. 1o <-> a = (/) )
187 fveq2 
 |-  ( a = (/) -> ( b ` a ) = ( b ` (/) ) )
188 186 187 sylbi 
 |-  ( a e. 1o -> ( b ` a ) = ( b ` (/) ) )
189 188 mpteq2dv 
 |-  ( a e. 1o -> ( b e. ( B ^m 1o ) |-> ( b ` a ) ) = ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) )
190 189 coeq1d 
 |-  ( 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 } ) ) ) )
191 190 eleq1d 
 |-  ( 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 } ) )
192 185 191 syl5ibrcom 
 |-  ( ph -> ( a e. 1o -> ( ( b e. ( B ^m 1o ) |-> ( b ` a ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } ) )
193 192 imp 
 |-  ( ( ph /\ a e. 1o ) -> ( ( b e. ( B ^m 1o ) |-> ( b ` a ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } )
194 4 1 38 pf1mpf 
 |-  ( A e. Q -> ( A o. ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) ) e. ran ( 1o eval R ) )
195 16 194 syl 
 |-  ( ph -> ( A o. ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) ) e. ran ( 1o eval R ) )
196 1 2 3 36 87 109 111 113 115 117 119 121 123 180 193 195 mpfind 
 |-  ( ph -> ( ( A o. ( b e. ( B ^m 1o ) |-> ( b ` (/) ) ) ) o. ( w e. B |-> ( 1o X. { w } ) ) ) e. { x | ps } )
197 33 196 eqeltrrd 
 |-  ( ph -> A e. { x | ps } )
198 13 elabg 
 |-  ( A e. Q -> ( A e. { x | ps } <-> rh ) )
199 16 198 syl 
 |-  ( ph -> ( A e. { x | ps } <-> rh ) )
200 197 199 mpbid 
 |-  ( ph -> rh )