Theorem mpfind 18808

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, 19-Mar-2015.)

Hypotheses

Ref	Expression
mpfind.cb	|- B = ( Base ` S )
mpfind.cp	|- .+ = ( +g ` S )
mpfind.ct	|- .x. = ( .r ` S )
mpfind.cq	|- Q = ran ( ( I evalSub S ) ` R )
mpfind.ad	|- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze )
mpfind.mu	|- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si )
mpfind.wa	|- ( x = ( ( B ^m I ) X. { f } ) -> ( ps <-> ch ) )
mpfind.wb	|- ( x = ( g e. ( B ^m I ) |-> ( g ` f ) ) -> ( ps <-> th ) )
mpfind.wc	|- ( x = f -> ( ps <-> ta ) )
mpfind.wd	|- ( x = g -> ( ps <-> et ) )
mpfind.we	|- ( x = ( f oF .+ g ) -> ( ps <-> ze ) )
mpfind.wf	|- ( x = ( f oF .x. g ) -> ( ps <-> si ) )
mpfind.wg	|- ( x = A -> ( ps <-> rh ) )
mpfind.co	|- ( ( ph /\ f e. R ) -> ch )
mpfind.pr	|- ( ( ph /\ f e. I ) -> th )
mpfind.a	|- ( ph -> A e. Q )

Assertion

Ref	Expression
mpfind	|- ( ph -> rh )

Distinct variable groups:   ch, x   et, x   ph, f, g   ps, f, g   rh, x   si, x   ta, x   th, x   ze, x   x, A   B, f, g, x   f, I, g, x   .+ , f, g, x   Q, f, g   R, f, g   S, f, g   .x. , f, g, x

Allowed substitution hints:   ph( x)   ps( x)   ch( f, g)   th( f, g)   ta( f, g)   et( f, g)   ze( f, g)   si( f, g)   rh( f, g)   A( f, g)   Q( x)   R( x)   S( x)

Proof of Theorem mpfind

Dummy variables i j y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpfind.a	. . . . 5 |- ( ph -> A e. Q )
2		mpfind.cq	. . . . 5 |- Q = ran ( ( I evalSub S ) ` R )
3	1, 2	syl6eleq 2550	. . . 4 |- ( ph -> A e. ran ( ( I evalSub S ) ` R ) )
4	2	mpfrcl 18790	. . . . . . . . 9 |- ( A e. Q -> ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) )
5	1, 4	syl 17	. . . . . . . 8 |- ( ph -> ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) )
6		eqid 2462	. . . . . . . . 9 |- ( ( I evalSub S ) ` R ) = ( ( I evalSub S ) ` R )
7		eqid 2462	. . . . . . . . 9 |- ( I mPoly ( S ↾s R ) ) = ( I mPoly ( S ↾s R ) )
8		eqid 2462	. . . . . . . . 9 |- ( S ↾s R ) = ( S ↾s R )
9		eqid 2462	. . . . . . . . 9 |- ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) )
10		mpfind.cb	. . . . . . . . 9 |- B = ( Base ` S )
11	6, 7, 8, 9, 10	evlsrhm 18793	. . . . . . . 8 |- ( ( I e. _V /\ S e. CRing /\ R e. (SubRing ` S ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( B ^m I ) ) ) )
12	5, 11	syl 17	. . . . . . 7 |- ( ph -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( B ^m I ) ) ) )
13		eqid 2462	. . . . . . . 8 |- ( Base ` ( I mPoly ( S ↾s R ) ) ) = ( Base ` ( I mPoly ( S ↾s R ) ) )
14		eqid 2462	. . . . . . . 8 |- ( Base ` ( S ^s ( B ^m I ) ) ) = ( Base ` ( S ^s ( B ^m I ) ) )
15	13, 14	rhmf 18003	. . . . . . 7 |- ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S ↾s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
16	12, 15	syl 17	. . . . . 6 |- ( ph -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S ↾s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
17		ffn 5751	. . . . . 6 |- ( ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S ↾s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) )
18	16, 17	syl 17	. . . . 5 |- ( ph -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) )
19		fvelrnb 5935	. . . . 5 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( A e. ran ( ( I evalSub S ) ` R ) <-> E. y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A ) )
20	18, 19	syl 17	. . . 4 |- ( ph -> ( A e. ran ( ( I evalSub S ) ` R ) <-> E. y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A ) )
21	3, 20	mpbid 215	. . 3 |- ( ph -> E. y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A )
22		ffun 5754	. . . . . . . 8 |- ( ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S ↾s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) -> Fun ( ( I evalSub S ) ` R ) )
23	16, 22	syl 17	. . . . . . 7 |- ( ph -> Fun ( ( I evalSub S ) ` R ) )
24	23	adantr 471	. . . . . 6 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> Fun ( ( I evalSub S ) ` R ) )
25		eqid 2462	. . . . . . 7 |- ( Base ` ( S ↾s R ) ) = ( Base ` ( S ↾s R ) )
26		eqid 2462	. . . . . . 7 |- ( I mVar ( S ↾s R ) ) = ( I mVar ( S ↾s R ) )
27		eqid 2462	. . . . . . 7 |- ( +g ` ( I mPoly ( S ↾s R ) ) ) = ( +g ` ( I mPoly ( S ↾s R ) ) )
28		eqid 2462	. . . . . . 7 |- ( .r ` ( I mPoly ( S ↾s R ) ) ) = ( .r ` ( I mPoly ( S ↾s R ) ) )
29		eqid 2462	. . . . . . 7 |- (algSc ` ( I mPoly ( S ↾s R ) ) ) = (algSc ` ( I mPoly ( S ↾s R ) ) )
30	5	simp1d 1026	. . . . . . . . . . . 12 |- ( ph -> I e. _V )
31	5	simp2d 1027	. . . . . . . . . . . . . 14 |- ( ph -> S e. CRing )
32	5	simp3d 1028	. . . . . . . . . . . . . 14 |- ( ph -> R e. (SubRing ` S ) )
33	8	subrgcrng 18061	. . . . . . . . . . . . . 14 |- ( ( S e. CRing /\ R e. (SubRing ` S ) ) -> ( S ↾s R ) e. CRing )
34	31, 32, 33	syl2anc 671	. . . . . . . . . . . . 13 |- ( ph -> ( S ↾s R ) e. CRing )
35		crngring 17840	. . . . . . . . . . . . 13 |- ( ( S ↾s R ) e. CRing -> ( S ↾s R ) e. Ring )
36	34, 35	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( S ↾s R ) e. Ring )
37	7	mplring 18725	. . . . . . . . . . . 12 |- ( ( I e. _V /\ ( S ↾s R ) e. Ring ) -> ( I mPoly ( S ↾s R ) ) e. Ring )
38	30, 36, 37	syl2anc 671	. . . . . . . . . . 11 |- ( ph -> ( I mPoly ( S ↾s R ) ) e. Ring )
39	38	adantr 471	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( I mPoly ( S ↾s R ) ) e. Ring )
40		simprl 769	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
41		elpreima 6025	. . . . . . . . . . . . . 14 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
42	18, 41	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
43	42	adantr 471	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
44	40, 43	mpbid 215	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
45	44	simpld 465	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
46		simprr 771	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
47		elpreima 6025	. . . . . . . . . . . . . 14 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
48	18, 47	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
49	48	adantr 471	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
50	46, 49	mpbid 215	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
51	50	simpld 465	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
52	13, 27	ringacl 17857	. . . . . . . . . 10 |- ( ( ( I mPoly ( S ↾s R ) ) e. Ring /\ i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
53	39, 45, 51, 52	syl3anc 1276	. . . . . . . . 9 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
54		rhmghm 18002	. . . . . . . . . . . . . 14 |- ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
55	12, 54	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
56	55	adantr 471	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) )
57		eqid 2462	. . . . . . . . . . . . 13 |- ( +g ` ( S ^s ( B ^m I ) ) ) = ( +g ` ( S ^s ( B ^m I ) ) )
58	13, 27, 57	ghmlin 16937	. . . . . . . . . . . 12 |- ( ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) GrpHom ( S ^s ( B ^m I ) ) ) /\ i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( +g ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
59	56, 45, 51, 58	syl3anc 1276	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( +g ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
60	31	adantr 471	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> S e. CRing )
61		ovex 6343	. . . . . . . . . . . . 13 |- ( B ^m I ) e. _V
62	61	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( B ^m I ) e. _V )
63	16	adantr 471	. . . . . . . . . . . . 13 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) : ( Base ` ( I mPoly ( S ↾s R ) ) ) --> ( Base ` ( S ^s ( B ^m I ) ) ) )
64	63, 45	ffvelrnd 6046	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. ( Base ` ( S ^s ( B ^m I ) ) ) )
65	63, 51	ffvelrnd 6046	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. ( Base ` ( S ^s ( B ^m I ) ) ) )
66		mpfind.cp	. . . . . . . . . . . 12 |- .+ = ( +g ` S )
67	9, 14, 60, 62, 64, 65, 66, 57	pwsplusgval 15437	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) ( +g ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) )
68	59, 67	eqtrd 2496	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) )
69		simpl 463	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ph )
70	18	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) )
71		fnfvelrn 6042	. . . . . . . . . . . . . 14 |- ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. ran ( ( I evalSub S ) ` R ) )
72	70, 45, 71	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. ran ( ( I evalSub S ) ` R ) )
73	72, 2	syl6eleqr 2551	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. Q )
74	23	adantr 471	. . . . . . . . . . . . 13 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> Fun ( ( I evalSub S ) ` R ) )
75		fvimacnvi 6019	. . . . . . . . . . . . 13 |- ( ( Fun ( ( I evalSub S ) ` R ) /\ i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } )
76	74, 40, 75	syl2anc 671	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } )
77	73, 76	jca 539	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
78		fnfvelrn 6042	. . . . . . . . . . . . . 14 |- ( ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. ran ( ( I evalSub S ) ` R ) )
79	70, 51, 78	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. ran ( ( I evalSub S ) ` R ) )
80	79, 2	syl6eleqr 2551	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. Q )
81		fvimacnvi 6019	. . . . . . . . . . . . 13 |- ( ( Fun ( ( I evalSub S ) ` R ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } )
82	74, 46, 81	syl2anc 671	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } )
83	80, 82	jca 539	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
84		fvex 5898	. . . . . . . . . . . 12 |- ( ( ( I evalSub S ) ` R ) ` i ) e. _V
85		fvex 5898	. . . . . . . . . . . 12 |- ( ( ( I evalSub S ) ` R ) ` j ) e. _V
86		eleq1 2528	. . . . . . . . . . . . . . . 16 |- ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( f e. Q <-> ( ( ( I evalSub S ) ` R ) ` i ) e. Q ) )
87		vex 3060	. . . . . . . . . . . . . . . . . 18 |- f e. _V
88		mpfind.wc	. . . . . . . . . . . . . . . . . 18 |- ( x = f -> ( ps <-> ta ) )
89	87, 88	elab 3197	. . . . . . . . . . . . . . . . 17 |- ( f e. { x | ps } <-> ta )
90		eleq1 2528	. . . . . . . . . . . . . . . . 17 |- ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( f e. { x | ps } <-> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
91	89, 90	syl5bbr 267	. . . . . . . . . . . . . . . 16 |- ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( ta <-> ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) )
92	86, 91	anbi12d 722	. . . . . . . . . . . . . . 15 |- ( f = ( ( ( I evalSub S ) ` R ) ` i ) -> ( ( f e. Q /\ ta ) <-> ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) ) )
93		eleq1 2528	. . . . . . . . . . . . . . . 16 |- ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( g e. Q <-> ( ( ( I evalSub S ) ` R ) ` j ) e. Q ) )
94		vex 3060	. . . . . . . . . . . . . . . . . 18 |- g e. _V
95		mpfind.wd	. . . . . . . . . . . . . . . . . 18 |- ( x = g -> ( ps <-> et ) )
96	94, 95	elab 3197	. . . . . . . . . . . . . . . . 17 |- ( g e. { x | ps } <-> et )
97		eleq1 2528	. . . . . . . . . . . . . . . . 17 |- ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( g e. { x | ps } <-> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
98	96, 97	syl5bbr 267	. . . . . . . . . . . . . . . 16 |- ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( et <-> ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) )
99	93, 98	anbi12d 722	. . . . . . . . . . . . . . 15 |- ( g = ( ( ( I evalSub S ) ` R ) ` j ) -> ( ( g e. Q /\ et ) <-> ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) )
100	92, 99	bi2anan9 889	. . . . . . . . . . . . . 14 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) <-> ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) )
101	100	anbi2d 715	. . . . . . . . . . . . 13 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) <-> ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) ) )
102		ovex 6343	. . . . . . . . . . . . . . 15 |- ( f oF .+ g ) e. _V
103		mpfind.we	. . . . . . . . . . . . . . 15 |- ( x = ( f oF .+ g ) -> ( ps <-> ze ) )
104	102, 103	elab 3197	. . . . . . . . . . . . . 14 |- ( ( f oF .+ g ) e. { x | ps } <-> ze )
105		oveq12 6324	. . . . . . . . . . . . . . 15 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( f oF .+ g ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) )
106	105	eleq1d 2524	. . . . . . . . . . . . . 14 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( f oF .+ g ) e. { x | ps } <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
107	104, 106	syl5bbr 267	. . . . . . . . . . . . 13 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ze <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
108	101, 107	imbi12d 326	. . . . . . . . . . . 12 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze ) <-> ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) ) )
109		mpfind.ad	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> ze )
110	84, 85, 108, 109	vtocl2 3114	. . . . . . . . . . 11 |- ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
111	69, 77, 83, 110	syl12anc 1274	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .+ ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
112	68, 111	eqeltrd 2540	. . . . . . . . 9 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } )
113		elpreima 6025	. . . . . . . . . . 11 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } ) ) )
114	18, 113	syl 17	. . . . . . . . . 10 |- ( ph -> ( ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } ) ) )
115	114	adantr 471	. . . . . . . . 9 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } ) ) )
116	53, 112, 115	mpbir2and 938	. . . . . . . 8 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
117	116	adantlr 726	. . . . . . 7 |- ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( +g ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
118	13, 28	ringcl 17843	. . . . . . . . . 10 |- ( ( ( I mPoly ( S ↾s R ) ) e. Ring /\ i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
119	39, 45, 51, 118	syl3anc 1276	. . . . . . . . 9 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
120		eqid 2462	. . . . . . . . . . . . . . 15 |- (mulGrp ` ( I mPoly ( S ↾s R ) ) ) = (mulGrp ` ( I mPoly ( S ↾s R ) ) )
121		eqid 2462	. . . . . . . . . . . . . . 15 |- (mulGrp ` ( S ^s ( B ^m I ) ) ) = (mulGrp ` ( S ^s ( B ^m I ) ) )
122	120, 121	rhmmhm 17999	. . . . . . . . . . . . . 14 |- ( ( ( I evalSub S ) ` R ) e. ( ( I mPoly ( S ↾s R ) ) RingHom ( S ^s ( B ^m I ) ) ) -> ( ( I evalSub S ) ` R ) e. ( (mulGrp ` ( I mPoly ( S ↾s R ) ) ) MndHom (mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
123	12, 122	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( ( I evalSub S ) ` R ) e. ( (mulGrp ` ( I mPoly ( S ↾s R ) ) ) MndHom (mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
124	123	adantr 471	. . . . . . . . . . . 12 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( I evalSub S ) ` R ) e. ( (mulGrp ` ( I mPoly ( S ↾s R ) ) ) MndHom (mulGrp ` ( S ^s ( B ^m I ) ) ) ) )
125	120, 13	mgpbas 17778	. . . . . . . . . . . . 13 |- ( Base ` ( I mPoly ( S ↾s R ) ) ) = ( Base ` (mulGrp ` ( I mPoly ( S ↾s R ) ) ) )
126	120, 28	mgpplusg 17776	. . . . . . . . . . . . 13 |- ( .r ` ( I mPoly ( S ↾s R ) ) ) = ( +g ` (mulGrp ` ( I mPoly ( S ↾s R ) ) ) )
127		eqid 2462	. . . . . . . . . . . . . 14 |- ( .r ` ( S ^s ( B ^m I ) ) ) = ( .r ` ( S ^s ( B ^m I ) ) )
128	121, 127	mgpplusg 17776	. . . . . . . . . . . . 13 |- ( .r ` ( S ^s ( B ^m I ) ) ) = ( +g ` (mulGrp ` ( S ^s ( B ^m I ) ) ) )
129	125, 126, 128	mhmlin 16638	. . . . . . . . . . . 12 |- ( ( ( ( I evalSub S ) ` R ) e. ( (mulGrp ` ( I mPoly ( S ↾s R ) ) ) MndHom (mulGrp ` ( S ^s ( B ^m I ) ) ) ) /\ i e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ j e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( .r ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
130	124, 45, 51, 129	syl3anc 1276	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) ( .r ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) )
131		mpfind.ct	. . . . . . . . . . . 12 |- .x. = ( .r ` S )
132	9, 14, 60, 62, 64, 65, 131, 127	pwsmulrval 15438	. . . . . . . . . . 11 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) ( .r ` ( S ^s ( B ^m I ) ) ) ( ( ( I evalSub S ) ` R ) ` j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) )
133	130, 132	eqtrd 2496	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) )
134		ovex 6343	. . . . . . . . . . . . . . 15 |- ( f oF .x. g ) e. _V
135		mpfind.wf	. . . . . . . . . . . . . . 15 |- ( x = ( f oF .x. g ) -> ( ps <-> si ) )
136	134, 135	elab 3197	. . . . . . . . . . . . . 14 |- ( ( f oF .x. g ) e. { x | ps } <-> si )
137		oveq12 6324	. . . . . . . . . . . . . . 15 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( f oF .x. g ) = ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) )
138	137	eleq1d 2524	. . . . . . . . . . . . . 14 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( f oF .x. g ) e. { x | ps } <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
139	136, 138	syl5bbr 267	. . . . . . . . . . . . 13 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( si <-> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) )
140	101, 139	imbi12d 326	. . . . . . . . . . . 12 |- ( ( f = ( ( ( I evalSub S ) ` R ) ` i ) /\ g = ( ( ( I evalSub S ) ` R ) ` j ) ) -> ( ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si ) <-> ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } ) ) )
141		mpfind.mu	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( f e. Q /\ ta ) /\ ( g e. Q /\ et ) ) ) -> si )
142	84, 85, 140, 141	vtocl2 3114	. . . . . . . . . . 11 |- ( ( ph /\ ( ( ( ( ( I evalSub S ) ` R ) ` i ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` i ) e. { x | ps } ) /\ ( ( ( ( I evalSub S ) ` R ) ` j ) e. Q /\ ( ( ( I evalSub S ) ` R ) ` j ) e. { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
143	69, 77, 83, 142	syl12anc 1274	. . . . . . . . . 10 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` i ) oF .x. ( ( ( I evalSub S ) ` R ) ` j ) ) e. { x | ps } )
144	133, 143	eqeltrd 2540	. . . . . . . . 9 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } )
145		elpreima 6025	. . . . . . . . . . 11 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } ) ) )
146	18, 145	syl 17	. . . . . . . . . 10 |- ( ph -> ( ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } ) ) )
147	146	adantr 471	. . . . . . . . 9 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) ) e. { x | ps } ) ) )
148	119, 144, 147	mpbir2and 938	. . . . . . . 8 |- ( ( ph /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
149	148	adantlr 726	. . . . . . 7 |- ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) /\ ( i e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) /\ j e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) ) -> ( i ( .r ` ( I mPoly ( S ↾s R ) ) ) j ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
150	7	mplassa 18727	. . . . . . . . . . . . . 14 |- ( ( I e. _V /\ ( S ↾s R ) e. CRing ) -> ( I mPoly ( S ↾s R ) ) e. AssAlg )
151	30, 34, 150	syl2anc 671	. . . . . . . . . . . . 13 |- ( ph -> ( I mPoly ( S ↾s R ) ) e. AssAlg )
152		eqid 2462	. . . . . . . . . . . . . 14 |- (Scalar ` ( I mPoly ( S ↾s R ) ) ) = (Scalar ` ( I mPoly ( S ↾s R ) ) )
153	29, 152	asclrhm 18615	. . . . . . . . . . . . 13 |- ( ( I mPoly ( S ↾s R ) ) e. AssAlg -> (algSc ` ( I mPoly ( S ↾s R ) ) ) e. ( (Scalar ` ( I mPoly ( S ↾s R ) ) ) RingHom ( I mPoly ( S ↾s R ) ) ) )
154	151, 153	syl 17	. . . . . . . . . . . 12 |- ( ph -> (algSc ` ( I mPoly ( S ↾s R ) ) ) e. ( (Scalar ` ( I mPoly ( S ↾s R ) ) ) RingHom ( I mPoly ( S ↾s R ) ) ) )
155		eqid 2462	. . . . . . . . . . . . 13 |- ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) = ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) )
156	155, 13	rhmf 18003	. . . . . . . . . . . 12 |- ( (algSc ` ( I mPoly ( S ↾s R ) ) ) e. ( (Scalar ` ( I mPoly ( S ↾s R ) ) ) RingHom ( I mPoly ( S ↾s R ) ) ) -> (algSc ` ( I mPoly ( S ↾s R ) ) ) : ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) --> ( Base ` ( I mPoly ( S ↾s R ) ) ) )
157	154, 156	syl 17	. . . . . . . . . . 11 |- ( ph -> (algSc ` ( I mPoly ( S ↾s R ) ) ) : ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) --> ( Base ` ( I mPoly ( S ↾s R ) ) ) )
158	157	adantr 471	. . . . . . . . . 10 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> (algSc ` ( I mPoly ( S ↾s R ) ) ) : ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) --> ( Base ` ( I mPoly ( S ↾s R ) ) ) )
159	7, 30, 34	mplsca 18718	. . . . . . . . . . . . 13 |- ( ph -> ( S ↾s R ) = (Scalar ` ( I mPoly ( S ↾s R ) ) ) )
160	159	fveq2d 5892	. . . . . . . . . . . 12 |- ( ph -> ( Base ` ( S ↾s R ) ) = ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) )
161	160	eleq2d 2525	. . . . . . . . . . 11 |- ( ph -> ( i e. ( Base ` ( S ↾s R ) ) <-> i e. ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) ) )
162	161	biimpa 491	. . . . . . . . . 10 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> i e. ( Base ` (Scalar ` ( I mPoly ( S ↾s R ) ) ) ) )
163	158, 162	ffvelrnd 6046	. . . . . . . . 9 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
164	30	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> I e. _V )
165	31	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> S e. CRing )
166	32	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> R e. (SubRing ` S ) )
167	10	subrgss 18058	. . . . . . . . . . . . . . 15 |- ( R e. (SubRing ` S ) -> R C_ B )
168	32, 167	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> R C_ B )
169	8, 10	ressbas2 15229	. . . . . . . . . . . . . 14 |- ( R C_ B -> R = ( Base ` ( S ↾s R ) ) )
170	168, 169	syl 17	. . . . . . . . . . . . 13 |- ( ph -> R = ( Base ` ( S ↾s R ) ) )
171	170	eleq2d 2525	. . . . . . . . . . . 12 |- ( ph -> ( i e. R <-> i e. ( Base ` ( S ↾s R ) ) ) )
172	171	biimpar 492	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> i e. R )
173	6, 7, 8, 10, 29, 164, 165, 166, 172	evlssca 18794	. . . . . . . . . 10 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) ) = ( ( B ^m I ) X. { i } ) )
174		mpfind.co	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. R ) -> ch )
175	174	ralrimiva 2814	. . . . . . . . . . . . 13 |- ( ph -> A. f e. R ch )
176		snex 4655	. . . . . . . . . . . . . . . . 17 |- { f } e. _V
177	61, 176	xpex 6622	. . . . . . . . . . . . . . . 16 |- ( ( B ^m I ) X. { f } ) e. _V
178		mpfind.wa	. . . . . . . . . . . . . . . 16 |- ( x = ( ( B ^m I ) X. { f } ) -> ( ps <-> ch ) )
179	177, 178	elab 3197	. . . . . . . . . . . . . . 15 |- ( ( ( B ^m I ) X. { f } ) e. { x | ps } <-> ch )
180		sneq 3990	. . . . . . . . . . . . . . . . 17 |- ( f = i -> { f } = { i } )
181	180	xpeq2d 4877	. . . . . . . . . . . . . . . 16 |- ( f = i -> ( ( B ^m I ) X. { f } ) = ( ( B ^m I ) X. { i } ) )
182	181	eleq1d 2524	. . . . . . . . . . . . . . 15 |- ( f = i -> ( ( ( B ^m I ) X. { f } ) e. { x | ps } <-> ( ( B ^m I ) X. { i } ) e. { x | ps } ) )
183	179, 182	syl5bbr 267	. . . . . . . . . . . . . 14 |- ( f = i -> ( ch <-> ( ( B ^m I ) X. { i } ) e. { x | ps } ) )
184	183	cbvralv 3031	. . . . . . . . . . . . 13 |- ( A. f e. R ch <-> A. i e. R ( ( B ^m I ) X. { i } ) e. { x | ps } )
185	175, 184	sylib 201	. . . . . . . . . . . 12 |- ( ph -> A. i e. R ( ( B ^m I ) X. { i } ) e. { x | ps } )
186	185	r19.21bi 2769	. . . . . . . . . . 11 |- ( ( ph /\ i e. R ) -> ( ( B ^m I ) X. { i } ) e. { x | ps } )
187	172, 186	syldan 477	. . . . . . . . . 10 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( ( B ^m I ) X. { i } ) e. { x | ps } )
188	173, 187	eqeltrd 2540	. . . . . . . . 9 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( ( ( I evalSub S ) ` R ) ` ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) ) e. { x | ps } )
189		elpreima 6025	. . . . . . . . . . 11 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) ) e. { x | ps } ) ) )
190	18, 189	syl 17	. . . . . . . . . 10 |- ( ph -> ( ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) ) e. { x | ps } ) ) )
191	190	adantr 471	. . . . . . . . 9 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) ) e. { x | ps } ) ) )
192	163, 188, 191	mpbir2and 938	. . . . . . . 8 |- ( ( ph /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
193	192	adantlr 726	. . . . . . 7 |- ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) /\ i e. ( Base ` ( S ↾s R ) ) ) -> ( (algSc ` ( I mPoly ( S ↾s R ) ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
194	30	adantr 471	. . . . . . . . . 10 |- ( ( ph /\ i e. I ) -> I e. _V )
195	36	adantr 471	. . . . . . . . . 10 |- ( ( ph /\ i e. I ) -> ( S ↾s R ) e. Ring )
196		simpr 467	. . . . . . . . . 10 |- ( ( ph /\ i e. I ) -> i e. I )
197	7, 26, 13, 194, 195, 196	mvrcl 18722	. . . . . . . . 9 |- ( ( ph /\ i e. I ) -> ( ( I mVar ( S ↾s R ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
198	31	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ i e. I ) -> S e. CRing )
199	32	adantr 471	. . . . . . . . . . 11 |- ( ( ph /\ i e. I ) -> R e. (SubRing ` S ) )
200	6, 26, 8, 10, 194, 198, 199, 196	evlsvar 18795	. . . . . . . . . 10 |- ( ( ph /\ i e. I ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S ↾s R ) ) ` i ) ) = ( g e. ( B ^m I ) |-> ( g ` i ) ) )
201		mpfind.pr	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. I ) -> th )
202	61	mptex 6161	. . . . . . . . . . . . . . 15 |- ( g e. ( B ^m I ) |-> ( g ` f ) ) e. _V
203		mpfind.wb	. . . . . . . . . . . . . . 15 |- ( x = ( g e. ( B ^m I ) |-> ( g ` f ) ) -> ( ps <-> th ) )
204	202, 203	elab 3197	. . . . . . . . . . . . . 14 |- ( ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> th )
205	201, 204	sylibr 217	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. I ) -> ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } )
206	205	ralrimiva 2814	. . . . . . . . . . . 12 |- ( ph -> A. f e. I ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } )
207		fveq2 5888	. . . . . . . . . . . . . . 15 |- ( f = i -> ( g ` f ) = ( g ` i ) )
208	207	mpteq2dv 4504	. . . . . . . . . . . . . 14 |- ( f = i -> ( g e. ( B ^m I ) |-> ( g ` f ) ) = ( g e. ( B ^m I ) |-> ( g ` i ) ) )
209	208	eleq1d 2524	. . . . . . . . . . . . 13 |- ( f = i -> ( ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } ) )
210	209	cbvralv 3031	. . . . . . . . . . . 12 |- ( A. f e. I ( g e. ( B ^m I ) |-> ( g ` f ) ) e. { x | ps } <-> A. i e. I ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
211	206, 210	sylib 201	. . . . . . . . . . 11 |- ( ph -> A. i e. I ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
212	211	r19.21bi 2769	. . . . . . . . . 10 |- ( ( ph /\ i e. I ) -> ( g e. ( B ^m I ) |-> ( g ` i ) ) e. { x | ps } )
213	200, 212	eqeltrd 2540	. . . . . . . . 9 |- ( ( ph /\ i e. I ) -> ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S ↾s R ) ) ` i ) ) e. { x | ps } )
214		elpreima 6025	. . . . . . . . . . 11 |- ( ( ( I evalSub S ) ` R ) Fn ( Base ` ( I mPoly ( S ↾s R ) ) ) -> ( ( ( I mVar ( S ↾s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( I mVar ( S ↾s R ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S ↾s R ) ) ` i ) ) e. { x | ps } ) ) )
215	18, 214	syl 17	. . . . . . . . . 10 |- ( ph -> ( ( ( I mVar ( S ↾s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( I mVar ( S ↾s R ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S ↾s R ) ) ` i ) ) e. { x | ps } ) ) )
216	215	adantr 471	. . . . . . . . 9 |- ( ( ph /\ i e. I ) -> ( ( ( I mVar ( S ↾s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) <-> ( ( ( I mVar ( S ↾s R ) ) ` i ) e. ( Base ` ( I mPoly ( S ↾s R ) ) ) /\ ( ( ( I evalSub S ) ` R ) ` ( ( I mVar ( S ↾s R ) ) ` i ) ) e. { x | ps } ) ) )
217	197, 213, 216	mpbir2and 938	. . . . . . . 8 |- ( ( ph /\ i e. I ) -> ( ( I mVar ( S ↾s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
218	217	adantlr 726	. . . . . . 7 |- ( ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) /\ i e. I ) -> ( ( I mVar ( S ↾s R ) ) ` i ) e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
219		simpr 467	. . . . . . 7 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) )
220	30	adantr 471	. . . . . . 7 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> I e. _V )
221	34	adantr 471	. . . . . . 7 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( S ↾s R ) e. CRing )
222	25, 26, 7, 27, 28, 29, 13, 117, 149, 193, 218, 219, 220, 221	mplind 18774	. . . . . 6 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> y e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) )
223		fvimacnvi 6019	. . . . . 6 |- ( ( Fun ( ( I evalSub S ) ` R ) /\ y e. ( `' ( ( I evalSub S ) ` R ) " { x | ps } ) ) -> ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } )
224	24, 222, 223	syl2anc 671	. . . . 5 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } )
225		eleq1 2528	. . . . 5 |- ( ( ( ( I evalSub S ) ` R ) ` y ) = A -> ( ( ( ( I evalSub S ) ` R ) ` y ) e. { x | ps } <-> A e. { x | ps } ) )
226	224, 225	syl5ibcom 228	. . . 4 |- ( ( ph /\ y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ) -> ( ( ( ( I evalSub S ) ` R ) ` y ) = A -> A e. { x | ps } ) )
227	226	rexlimdva 2891	. . 3 |- ( ph -> ( E. y e. ( Base ` ( I mPoly ( S ↾s R ) ) ) ( ( ( I evalSub S ) ` R ) ` y ) = A -> A e. { x | ps } ) )
228	21, 227	mpd 15	. 2 |- ( ph -> A e. { x | ps } )
229		mpfind.wg	. . . 4 |- ( x = A -> ( ps <-> rh ) )
230	229	elabg 3198	. . 3 |- ( A e. Q -> ( A e. { x | ps } <-> rh ) )
231	1, 230	syl 17	. 2 |- ( ph -> ( A e. { x | ps } <-> rh ) )
232	228, 231	mpbid 215	1 |- ( ph -> rh )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   {cab 2448   A.wral 2749   E.wrex 2750   _Vcvv 3057   C_ wss 3416   {csn 3980   |-> cmpt 4475   X. cxp 4851   `'ccnv 4852   ran crn 4854   "cima 4856   Fun wfun 5595   Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315   oFcof 6556   ^m cmap 7498   Basecbs 15170   ↾_s cress 15171   +g cplusg 15239   .rcmulr 15240  Scalarcsca 15242   ^_s cpws 15394   MndHom cmhm 16629   GrpHom cghm 16929  mulGrpcmgp 17772   Ringcrg 17829   CRingccrg 17830   RingHom crh 17989  SubRingcsubrg 18053  AssAlgcasa 18582  algSccascl 18584   mVar cmvr 18625   mPoly cmpl 18626   evalSub ces 18776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-ofr 6559  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-sup 7982  df-oi 8051  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-fz 11814  df-fzo 11947  df-seq 12246  df-hash 12548  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-sca 15255  df-vsca 15256  df-ip 15257  df-tset 15258  df-ple 15259  df-ds 15261  df-hom 15263  df-cco 15264  df-0g 15389  df-gsum 15390  df-prds 15395  df-pws 15397  df-mre 15541  df-mrc 15542  df-acs 15544  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-mhm 16631  df-submnd 16632  df-grp 16722  df-minusg 16723  df-sbg 16724  df-mulg 16725  df-subg 16863  df-ghm 16930  df-cntz 17020  df-cmn 17481  df-abl 17482  df-mgp 17773  df-ur 17785  df-srg 17789  df-ring 17831  df-cring 17832  df-rnghom 17992  df-subrg 18055  df-lmod 18142  df-lss 18205  df-lsp 18244  df-assa 18585  df-asp 18586  df-ascl 18587  df-psr 18629  df-mvr 18630  df-mpl 18631  df-evls 18778

This theorem is referenced by:  pf1ind  18992  mzpmfp  35634