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	syl5eq	|- ( 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	syl5bi	|- ( 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	syl5bi	|- ( 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	ffvelrnda	|- ( ( 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		snex	|- { 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 )