Theorem evlslem1 19515

Description: Lemma for evlseu 19516, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.)

Hypotheses

Ref	Expression
evlslem1.p	|- P = ( I mPoly R )
evlslem1.b	|- B = ( Base ` P )
evlslem1.c	|- C = ( Base ` S )
evlslem1.k	|- K = ( Base ` R )
evlslem1.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlslem1.t	|- T = (mulGrp ` S )
evlslem1.x	|- .^ = (.g ` T )
evlslem1.m	|- .x. = ( .r ` S )
evlslem1.v	|- V = ( I mVar R )
evlslem1.e	|- E = ( p e. B |-> ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
evlslem1.i	|- ( ph -> I e. _V )
evlslem1.r	|- ( ph -> R e. CRing )
evlslem1.s	|- ( ph -> S e. CRing )
evlslem1.f	|- ( ph -> F e. ( R RingHom S ) )
evlslem1.g	|- ( ph -> G : I --> C )
evlslem1.a	|- A = (algSc ` P )

Assertion

Ref	Expression
evlslem1	|- ( ph -> ( E e. ( P RingHom S ) /\ ( E o. A ) = F /\ ( E o. V ) = G ) )

Distinct variable groups:   p, b, B   C, b, p   ph, b, p   F, b, p   K, b   T, b, p   D, b, p   h, b, I, p   R, b, h, p   G, b, p   P, b, p   S, b, p   .x. , b, p   .^ , b, p

Allowed substitution hints:   ph( h)   A( h, p, b)   B( h)   C( h)   D( h)   P( h)   S( h)   T( h)   .x. ( h)   E( h, p, b)   .^ ( h)   F( h)   G( h)   K( h, p)   V( h, p, b)

Proof of Theorem evlslem1

Dummy variables x v w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlslem1.b	. . 3 |- B = ( Base ` P )
2		eqid 2622	. . 3 |- ( 1r ` P ) = ( 1r ` P )
3		eqid 2622	. . 3 |- ( 1r ` S ) = ( 1r ` S )
4		eqid 2622	. . 3 |- ( .r ` P ) = ( .r ` P )
5		evlslem1.m	. . 3 |- .x. = ( .r ` S )
6		evlslem1.i	. . . 4 |- ( ph -> I e. _V )
7		evlslem1.r	. . . . 5 |- ( ph -> R e. CRing )
8		crngring 18558	. . . . 5 |- ( R e. CRing -> R e. Ring )
9	7, 8	syl 17	. . . 4 |- ( ph -> R e. Ring )
10		evlslem1.p	. . . . 5 |- P = ( I mPoly R )
11	10	mplring 19452	. . . 4 |- ( ( I e. _V /\ R e. Ring ) -> P e. Ring )
12	6, 9, 11	syl2anc 693	. . 3 |- ( ph -> P e. Ring )
13		evlslem1.s	. . . 4 |- ( ph -> S e. CRing )
14		crngring 18558	. . . 4 |- ( S e. CRing -> S e. Ring )
15	13, 14	syl 17	. . 3 |- ( ph -> S e. Ring )
16		fveq2 6191	. . . . . . 7 |- ( x = ( 1r ` R ) -> ( A ` x ) = ( A ` ( 1r ` R ) ) )
17	16	fveq2d 6195	. . . . . 6 |- ( x = ( 1r ` R ) -> ( E ` ( A ` x ) ) = ( E ` ( A ` ( 1r ` R ) ) ) )
18		fveq2 6191	. . . . . 6 |- ( x = ( 1r ` R ) -> ( F ` x ) = ( F ` ( 1r ` R ) ) )
19	17, 18	eqeq12d 2637	. . . . 5 |- ( x = ( 1r ` R ) -> ( ( E ` ( A ` x ) ) = ( F ` x ) <-> ( E ` ( A ` ( 1r ` R ) ) ) = ( F ` ( 1r ` R ) ) ) )
20		evlslem1.d	. . . . . . . . 9 |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
21		eqid 2622	. . . . . . . . 9 |- ( 0g ` R ) = ( 0g ` R )
22		evlslem1.k	. . . . . . . . 9 |- K = ( Base ` R )
23		evlslem1.a	. . . . . . . . 9 |- A = (algSc ` P )
24	6	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. K ) -> I e. _V )
25	9	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. K ) -> R e. Ring )
26		simpr 477	. . . . . . . . 9 |- ( ( ph /\ x e. K ) -> x e. K )
27	10, 20, 21, 22, 23, 24, 25, 26	mplascl 19496	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> ( A ` x ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) )
28	27	fveq2d 6195	. . . . . . 7 |- ( ( ph /\ x e. K ) -> ( E ` ( A ` x ) ) = ( E ` ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) )
29		evlslem1.c	. . . . . . . 8 |- C = ( Base ` S )
30		evlslem1.t	. . . . . . . 8 |- T = (mulGrp ` S )
31		evlslem1.x	. . . . . . . 8 |- .^ = (.g ` T )
32		evlslem1.v	. . . . . . . 8 |- V = ( I mVar R )
33		evlslem1.e	. . . . . . . 8 |- E = ( p e. B |-> ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
34	7	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> R e. CRing )
35	13	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> S e. CRing )
36		evlslem1.f	. . . . . . . . 9 |- ( ph -> F e. ( R RingHom S ) )
37	36	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> F e. ( R RingHom S ) )
38		evlslem1.g	. . . . . . . . 9 |- ( ph -> G : I --> C )
39	38	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> G : I --> C )
40	20	psrbag0 19494	. . . . . . . . . 10 |- ( I e. _V -> ( I X. { 0 } ) e. D )
41	6, 40	syl 17	. . . . . . . . 9 |- ( ph -> ( I X. { 0 } ) e. D )
42	41	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> ( I X. { 0 } ) e. D )
43	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 24, 34, 35, 37, 39, 21, 42, 26	evlslem3 19514	. . . . . . 7 |- ( ( ph /\ x e. K ) -> ( E ` ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) = ( ( F ` x ) .x. ( T gsumg ( ( I X. { 0 } ) oF .^ G ) ) ) )
44		0zd 11389	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> 0 e. ZZ )
45		fvexd 6203	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> ( G ` x ) e. _V )
46		fconstmpt 5163	. . . . . . . . . . . . . . 15 |- ( I X. { 0 } ) = ( x e. I |-> 0 )
47	46	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( I X. { 0 } ) = ( x e. I |-> 0 ) )
48	38	feqmptd 6249	. . . . . . . . . . . . . 14 |- ( ph -> G = ( x e. I |-> ( G ` x ) ) )
49	6, 44, 45, 47, 48	offval2 6914	. . . . . . . . . . . . 13 |- ( ph -> ( ( I X. { 0 } ) oF .^ G ) = ( x e. I |-> ( 0 .^ ( G ` x ) ) ) )
50	38	ffvelrnda 6359	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. I ) -> ( G ` x ) e. C )
51	30, 29	mgpbas 18495	. . . . . . . . . . . . . . . 16 |- C = ( Base ` T )
52	30, 3	ringidval 18503	. . . . . . . . . . . . . . . 16 |- ( 1r ` S ) = ( 0g ` T )
53	51, 52, 31	mulg0 17546	. . . . . . . . . . . . . . 15 |- ( ( G ` x ) e. C -> ( 0 .^ ( G ` x ) ) = ( 1r ` S ) )
54	50, 53	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> ( 0 .^ ( G ` x ) ) = ( 1r ` S ) )
55	54	mpteq2dva 4744	. . . . . . . . . . . . 13 |- ( ph -> ( x e. I |-> ( 0 .^ ( G ` x ) ) ) = ( x e. I |-> ( 1r ` S ) ) )
56	49, 55	eqtrd 2656	. . . . . . . . . . . 12 |- ( ph -> ( ( I X. { 0 } ) oF .^ G ) = ( x e. I |-> ( 1r ` S ) ) )
57	56	oveq2d 6666	. . . . . . . . . . 11 |- ( ph -> ( T gsumg ( ( I X. { 0 } ) oF .^ G ) ) = ( T gsumg ( x e. I |-> ( 1r ` S ) ) ) )
58	30	crngmgp 18555	. . . . . . . . . . . . . 14 |- ( S e. CRing -> T e. CMnd )
59	13, 58	syl 17	. . . . . . . . . . . . 13 |- ( ph -> T e. CMnd )
60		cmnmnd 18208	. . . . . . . . . . . . 13 |- ( T e. CMnd -> T e. Mnd )
61	59, 60	syl 17	. . . . . . . . . . . 12 |- ( ph -> T e. Mnd )
62	52	gsumz 17374	. . . . . . . . . . . 12 |- ( ( T e. Mnd /\ I e. _V ) -> ( T gsumg ( x e. I |-> ( 1r ` S ) ) ) = ( 1r ` S ) )
63	61, 6, 62	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( T gsumg ( x e. I |-> ( 1r ` S ) ) ) = ( 1r ` S ) )
64	57, 63	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( T gsumg ( ( I X. { 0 } ) oF .^ G ) ) = ( 1r ` S ) )
65	64	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. K ) -> ( T gsumg ( ( I X. { 0 } ) oF .^ G ) ) = ( 1r ` S ) )
66	65	oveq2d 6666	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> ( ( F ` x ) .x. ( T gsumg ( ( I X. { 0 } ) oF .^ G ) ) ) = ( ( F ` x ) .x. ( 1r ` S ) ) )
67	22, 29	rhmf 18726	. . . . . . . . . . 11 |- ( F e. ( R RingHom S ) -> F : K --> C )
68	36, 67	syl 17	. . . . . . . . . 10 |- ( ph -> F : K --> C )
69	68	ffvelrnda 6359	. . . . . . . . 9 |- ( ( ph /\ x e. K ) -> ( F ` x ) e. C )
70	29, 5, 3	ringridm 18572	. . . . . . . . 9 |- ( ( S e. Ring /\ ( F ` x ) e. C ) -> ( ( F ` x ) .x. ( 1r ` S ) ) = ( F ` x ) )
71	15, 69, 70	syl2an2r 876	. . . . . . . 8 |- ( ( ph /\ x e. K ) -> ( ( F ` x ) .x. ( 1r ` S ) ) = ( F ` x ) )
72	66, 71	eqtrd 2656	. . . . . . 7 |- ( ( ph /\ x e. K ) -> ( ( F ` x ) .x. ( T gsumg ( ( I X. { 0 } ) oF .^ G ) ) ) = ( F ` x ) )
73	28, 43, 72	3eqtrd 2660	. . . . . 6 |- ( ( ph /\ x e. K ) -> ( E ` ( A ` x ) ) = ( F ` x ) )
74	73	ralrimiva 2966	. . . . 5 |- ( ph -> A. x e. K ( E ` ( A ` x ) ) = ( F ` x ) )
75		eqid 2622	. . . . . . 7 |- ( 1r ` R ) = ( 1r ` R )
76	22, 75	ringidcl 18568	. . . . . 6 |- ( R e. Ring -> ( 1r ` R ) e. K )
77	9, 76	syl 17	. . . . 5 |- ( ph -> ( 1r ` R ) e. K )
78	19, 74, 77	rspcdva 3316	. . . 4 |- ( ph -> ( E ` ( A ` ( 1r ` R ) ) ) = ( F ` ( 1r ` R ) ) )
79	10	mplassa 19454	. . . . . . . . 9 |- ( ( I e. _V /\ R e. CRing ) -> P e. AssAlg )
80	6, 7, 79	syl2anc 693	. . . . . . . 8 |- ( ph -> P e. AssAlg )
81		eqid 2622	. . . . . . . . 9 |- (Scalar ` P ) = (Scalar ` P )
82	23, 81	asclrhm 19342	. . . . . . . 8 |- ( P e. AssAlg -> A e. ( (Scalar ` P ) RingHom P ) )
83	80, 82	syl 17	. . . . . . 7 |- ( ph -> A e. ( (Scalar ` P ) RingHom P ) )
84	10, 6, 7	mplsca 19445	. . . . . . . 8 |- ( ph -> R = (Scalar ` P ) )
85	84	oveq1d 6665	. . . . . . 7 |- ( ph -> ( R RingHom P ) = ( (Scalar ` P ) RingHom P ) )
86	83, 85	eleqtrrd 2704	. . . . . 6 |- ( ph -> A e. ( R RingHom P ) )
87	75, 2	rhm1 18730	. . . . . 6 |- ( A e. ( R RingHom P ) -> ( A ` ( 1r ` R ) ) = ( 1r ` P ) )
88	86, 87	syl 17	. . . . 5 |- ( ph -> ( A ` ( 1r ` R ) ) = ( 1r ` P ) )
89	88	fveq2d 6195	. . . 4 |- ( ph -> ( E ` ( A ` ( 1r ` R ) ) ) = ( E ` ( 1r ` P ) ) )
90	75, 3	rhm1 18730	. . . . 5 |- ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
91	36, 90	syl 17	. . . 4 |- ( ph -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
92	78, 89, 91	3eqtr3d 2664	. . 3 |- ( ph -> ( E ` ( 1r ` P ) ) = ( 1r ` S ) )
93		eqid 2622	. . . . 5 |- ( +g ` P ) = ( +g ` P )
94		eqid 2622	. . . . 5 |- ( +g ` S ) = ( +g ` S )
95		ringgrp 18552	. . . . . 6 |- ( P e. Ring -> P e. Grp )
96	12, 95	syl 17	. . . . 5 |- ( ph -> P e. Grp )
97		ringgrp 18552	. . . . . 6 |- ( S e. Ring -> S e. Grp )
98	15, 97	syl 17	. . . . 5 |- ( ph -> S e. Grp )
99		eqid 2622	. . . . . . 7 |- ( 0g ` S ) = ( 0g ` S )
100		ringcmn 18581	. . . . . . . . 9 |- ( S e. Ring -> S e. CMnd )
101	15, 100	syl 17	. . . . . . . 8 |- ( ph -> S e. CMnd )
102	101	adantr 481	. . . . . . 7 |- ( ( ph /\ p e. B ) -> S e. CMnd )
103		ovex 6678	. . . . . . . . 9 |- ( NN0 ^m I ) e. _V
104	20, 103	rabex2 4815	. . . . . . . 8 |- D e. _V
105	104	a1i 11	. . . . . . 7 |- ( ( ph /\ p e. B ) -> D e. _V )
106	6	adantr 481	. . . . . . . . 9 |- ( ( ph /\ p e. B ) -> I e. _V )
107	7	adantr 481	. . . . . . . . 9 |- ( ( ph /\ p e. B ) -> R e. CRing )
108	13	adantr 481	. . . . . . . . 9 |- ( ( ph /\ p e. B ) -> S e. CRing )
109	36	adantr 481	. . . . . . . . 9 |- ( ( ph /\ p e. B ) -> F e. ( R RingHom S ) )
110	38	adantr 481	. . . . . . . . 9 |- ( ( ph /\ p e. B ) -> G : I --> C )
111		simpr 477	. . . . . . . . 9 |- ( ( ph /\ p e. B ) -> p e. B )
112	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 106, 107, 108, 109, 110, 111	evlslem6 19513	. . . . . . . 8 |- ( ( ph /\ p e. B ) -> ( ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )
113	112	simpld 475	. . . . . . 7 |- ( ( ph /\ p e. B ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) : D --> C )
114	112	simprd 479	. . . . . . 7 |- ( ( ph /\ p e. B ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
115	29, 99, 102, 105, 113, 114	gsumcl 18316	. . . . . 6 |- ( ( ph /\ p e. B ) -> ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) e. C )
116	115, 33	fmptd 6385	. . . . 5 |- ( ph -> E : B --> C )
117		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( +g ` R ) = ( +g ` R )
118		simplrl 800	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> x e. B )
119		simplrr 801	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> y e. B )
120	10, 1, 117, 93, 118, 119	mpladd 19442	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( x ( +g ` P ) y ) = ( x oF ( +g ` R ) y ) )
121	120	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x ( +g ` P ) y ) ` b ) = ( ( x oF ( +g ` R ) y ) ` b ) )
122		simprl 794	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
123	10, 22, 1, 20, 122	mplelf 19433	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x : D --> K )
124	123	ffnd 6046	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x Fn D )
125	124	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> x Fn D )
126		simprr 796	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
127	10, 22, 1, 20, 126	mplelf 19433	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y : D --> K )
128	127	ffnd 6046	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y Fn D )
129	128	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> y Fn D )
130	104	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> D e. _V )
131		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> b e. D )
132		fnfvof 6911	. . . . . . . . . . . . . . . 16 |- ( ( ( x Fn D /\ y Fn D ) /\ ( D e. _V /\ b e. D ) ) -> ( ( x oF ( +g ` R ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) )
133	125, 129, 130, 131, 132	syl22anc 1327	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x oF ( +g ` R ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) )
134	121, 133	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x ( +g ` P ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) )
135	134	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ( +g ` P ) y ) ` b ) ) = ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) )
136		rhmghm 18725	. . . . . . . . . . . . . . . 16 |- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
137	36, 136	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> F e. ( R GrpHom S ) )
138	137	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> F e. ( R GrpHom S ) )
139	123	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( x ` b ) e. K )
140	127	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( y ` b ) e. K )
141	22, 117, 94	ghmlin 17665	. . . . . . . . . . . . . 14 |- ( ( F e. ( R GrpHom S ) /\ ( x ` b ) e. K /\ ( y ` b ) e. K ) -> ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) )
142	138, 139, 140, 141	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) )
143	135, 142	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ( +g ` P ) y ) ` b ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) )
144	143	oveq1d 6665	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsumg ( b oF .^ G ) ) ) )
145	15	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> S e. Ring )
146	68	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> F : K --> C )
147	146, 139	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( x ` b ) ) e. C )
148	146, 140	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( y ` b ) ) e. C )
149	59	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> T e. CMnd )
150	38	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> G : I --> C )
151	6	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> I e. _V )
152	20, 51, 31, 52, 149, 131, 150, 151	psrbagev2 19511	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( T gsumg ( b oF .^ G ) ) e. C )
153	29, 94, 5	ringdir 18567	. . . . . . . . . . . 12 |- ( ( S e. Ring /\ ( ( F ` ( x ` b ) ) e. C /\ ( F ` ( y ` b ) ) e. C /\ ( T gsumg ( b oF .^ G ) ) e. C ) ) -> ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
154	145, 147, 148, 152, 153	syl13anc 1328	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
155	144, 154	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
156	155	mpteq2dva 4744	. . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
157	104	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. _V )
158		ovexd 6680	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) e. _V )
159		ovexd 6680	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) e. _V )
160		eqidd 2623	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
161		eqidd 2623	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
162	157, 158, 159, 160, 161	offval2 6914	. . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) = ( b e. D |-> ( ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
163	156, 162	eqtr4d 2659	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
164	163	oveq2d 6666	. . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsumg ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) = ( S gsumg ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ) )
165	101	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. CMnd )
166	6	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> I e. _V )
167	7	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> R e. CRing )
168	13	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. CRing )
169	36	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F e. ( R RingHom S ) )
170	38	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> G : I --> C )
171	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 166, 167, 168, 169, 170, 122	evlslem6 19513	. . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )
172	171	simpld 475	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) : D --> C )
173	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 166, 167, 168, 169, 170, 126	evlslem6 19513	. . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )
174	173	simpld 475	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) : D --> C )
175	171	simprd 479	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
176	173	simprd 479	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
177	29, 99, 94, 165, 157, 172, 174, 175, 176	gsumadd 18323	. . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsumg ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ) = ( ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ) )
178	164, 177	eqtrd 2656	. . . . . 6 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsumg ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) = ( ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ) )
179	96	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> P e. Grp )
180	1, 93	grpcl 17430	. . . . . . . 8 |- ( ( P e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` P ) y ) e. B )
181	179, 122, 126, 180	syl3anc 1326	. . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` P ) y ) e. B )
182		fveq1 6190	. . . . . . . . . . . 12 |- ( p = ( x ( +g ` P ) y ) -> ( p ` b ) = ( ( x ( +g ` P ) y ) ` b ) )
183	182	fveq2d 6195	. . . . . . . . . . 11 |- ( p = ( x ( +g ` P ) y ) -> ( F ` ( p ` b ) ) = ( F ` ( ( x ( +g ` P ) y ) ` b ) ) )
184	183	oveq1d 6665	. . . . . . . . . 10 |- ( p = ( x ( +g ` P ) y ) -> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) )
185	184	mpteq2dv 4745	. . . . . . . . 9 |- ( p = ( x ( +g ` P ) y ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
186	185	oveq2d 6666	. . . . . . . 8 |- ( p = ( x ( +g ` P ) y ) -> ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) = ( S gsumg ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
187		ovex 6678	. . . . . . . 8 |- ( S gsumg ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) e. _V
188	186, 33, 187	fvmpt 6282	. . . . . . 7 |- ( ( x ( +g ` P ) y ) e. B -> ( E ` ( x ( +g ` P ) y ) ) = ( S gsumg ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
189	181, 188	syl 17	. . . . . 6 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( +g ` P ) y ) ) = ( S gsumg ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
190		fveq1 6190	. . . . . . . . . . . . 13 |- ( p = x -> ( p ` b ) = ( x ` b ) )
191	190	fveq2d 6195	. . . . . . . . . . . 12 |- ( p = x -> ( F ` ( p ` b ) ) = ( F ` ( x ` b ) ) )
192	191	oveq1d 6665	. . . . . . . . . . 11 |- ( p = x -> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) )
193	192	mpteq2dv 4745	. . . . . . . . . 10 |- ( p = x -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
194	193	oveq2d 6666	. . . . . . . . 9 |- ( p = x -> ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) = ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
195		ovex 6678	. . . . . . . . 9 |- ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) e. _V
196	194, 33, 195	fvmpt 6282	. . . . . . . 8 |- ( x e. B -> ( E ` x ) = ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
197	122, 196	syl 17	. . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` x ) = ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
198		fveq1 6190	. . . . . . . . . . . . 13 |- ( p = y -> ( p ` b ) = ( y ` b ) )
199	198	fveq2d 6195	. . . . . . . . . . . 12 |- ( p = y -> ( F ` ( p ` b ) ) = ( F ` ( y ` b ) ) )
200	199	oveq1d 6665	. . . . . . . . . . 11 |- ( p = y -> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) = ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) )
201	200	mpteq2dv 4745	. . . . . . . . . 10 |- ( p = y -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) )
202	201	oveq2d 6666	. . . . . . . . 9 |- ( p = y -> ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) = ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
203		ovex 6678	. . . . . . . . 9 |- ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) e. _V
204	202, 33, 203	fvmpt 6282	. . . . . . . 8 |- ( y e. B -> ( E ` y ) = ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
205	204	ad2antll 765	. . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` y ) = ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) )
206	197, 205	oveq12d 6668	. . . . . 6 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( E ` x ) ( +g ` S ) ( E ` y ) ) = ( ( S gsumg ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsumg ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) ) )
207	178, 189, 206	3eqtr4d 2666	. . . . 5 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( +g ` P ) y ) ) = ( ( E ` x ) ( +g ` S ) ( E ` y ) ) )
208	1, 29, 93, 94, 96, 98, 116, 207	isghmd 17669	. . . 4 |- ( ph -> E e. ( P GrpHom S ) )
209		eqid 2622	. . . . . . . . . . 11 |- (mulGrp ` R ) = (mulGrp ` R )
210	209, 30	rhmmhm 18722	. . . . . . . . . 10 |- ( F e. ( R RingHom S ) -> F e. ( (mulGrp ` R ) MndHom T ) )
211	36, 210	syl 17	. . . . . . . . 9 |- ( ph -> F e. ( (mulGrp ` R ) MndHom T ) )
212	211	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F e. ( (mulGrp ` R ) MndHom T ) )
213		simprll 802	. . . . . . . . . 10 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> x e. B )
214	10, 22, 1, 20, 213	mplelf 19433	. . . . . . . . 9 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> x : D --> K )
215		simprrl 804	. . . . . . . . 9 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> z e. D )
216	214, 215	ffvelrnd 6360	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( x ` z ) e. K )
217		simprlr 803	. . . . . . . . . 10 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> y e. B )
218	10, 22, 1, 20, 217	mplelf 19433	. . . . . . . . 9 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> y : D --> K )
219		simprrr 805	. . . . . . . . 9 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> w e. D )
220	218, 219	ffvelrnd 6360	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( y ` w ) e. K )
221	209, 22	mgpbas 18495	. . . . . . . . 9 |- K = ( Base ` (mulGrp ` R ) )
222		eqid 2622	. . . . . . . . . 10 |- ( .r ` R ) = ( .r ` R )
223	209, 222	mgpplusg 18493	. . . . . . . . 9 |- ( .r ` R ) = ( +g ` (mulGrp ` R ) )
224	30, 5	mgpplusg 18493	. . . . . . . . 9 |- .x. = ( +g ` T )
225	221, 223, 224	mhmlin 17342	. . . . . . . 8 |- ( ( F e. ( (mulGrp ` R ) MndHom T ) /\ ( x ` z ) e. K /\ ( y ` w ) e. K ) -> ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) )
226	212, 216, 220, 225	syl3anc 1326	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) )
227	61	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> T e. Mnd )
228		simprl 794	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> z e. D )
229	20	psrbagf 19365	. . . . . . . . . . . . . . 15 |- ( ( I e. _V /\ z e. D ) -> z : I --> NN0 )
230	6, 228, 229	syl2an2r 876	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> z : I --> NN0 )
231	230	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( z ` v ) e. NN0 )
232		simprr 796	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> w e. D )
233	20	psrbagf 19365	. . . . . . . . . . . . . . 15 |- ( ( I e. _V /\ w e. D ) -> w : I --> NN0 )
234	6, 232, 233	syl2an2r 876	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> w : I --> NN0 )
235	234	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( w ` v ) e. NN0 )
236	38	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> G : I --> C )
237	236	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) e. C )
238	51, 31, 224	mulgnn0dir 17571	. . . . . . . . . . . . 13 |- ( ( T e. Mnd /\ ( ( z ` v ) e. NN0 /\ ( w ` v ) e. NN0 /\ ( G ` v ) e. C ) ) -> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) = ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) )
239	227, 231, 235, 237, 238	syl13anc 1328	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) = ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) )
240	239	mpteq2dva 4744	. . . . . . . . . . 11 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( v e. I |-> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) ) = ( v e. I |-> ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) )
241	6	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> I e. _V )
242		ovexd 6680	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( z ` v ) + ( w ` v ) ) e. _V )
243		fvexd 6203	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) e. _V )
244	230	ffnd 6046	. . . . . . . . . . . . 13 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> z Fn I )
245	234	ffnd 6046	. . . . . . . . . . . . 13 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> w Fn I )
246		inidm 3822	. . . . . . . . . . . . 13 |- ( I i^i I ) = I
247		eqidd 2623	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( z ` v ) = ( z ` v ) )
248		eqidd 2623	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( w ` v ) = ( w ` v ) )
249	244, 245, 241, 241, 246, 247, 248	offval 6904	. . . . . . . . . . . 12 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF + w ) = ( v e. I |-> ( ( z ` v ) + ( w ` v ) ) ) )
250	38	feqmptd 6249	. . . . . . . . . . . . 13 |- ( ph -> G = ( v e. I |-> ( G ` v ) ) )
251	250	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> G = ( v e. I |-> ( G ` v ) ) )
252	241, 242, 243, 249, 251	offval2 6914	. . . . . . . . . . 11 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF + w ) oF .^ G ) = ( v e. I |-> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) ) )
253		ovexd 6680	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( z ` v ) .^ ( G ` v ) ) e. _V )
254		ovexd 6680	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( w ` v ) .^ ( G ` v ) ) e. _V )
255	38	ffnd 6046	. . . . . . . . . . . . . 14 |- ( ph -> G Fn I )
256	255	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> G Fn I )
257		eqidd 2623	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) = ( G ` v ) )
258	244, 256, 241, 241, 246, 247, 257	offval 6904	. . . . . . . . . . . 12 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) = ( v e. I |-> ( ( z ` v ) .^ ( G ` v ) ) ) )
259	245, 256, 241, 241, 246, 248, 257	offval 6904	. . . . . . . . . . . 12 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) = ( v e. I |-> ( ( w ` v ) .^ ( G ` v ) ) ) )
260	241, 253, 254, 258, 259	offval2 6914	. . . . . . . . . . 11 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) = ( v e. I |-> ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) )
261	240, 252, 260	3eqtr4d 2666	. . . . . . . . . 10 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF + w ) oF .^ G ) = ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) )
262	261	oveq2d 6666	. . . . . . . . 9 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsumg ( ( z oF + w ) oF .^ G ) ) = ( T gsumg ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) )
263	59	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> T e. CMnd )
264	20, 51, 31, 52, 263, 228, 236, 241	psrbagev1 19510	. . . . . . . . . . 11 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF .^ G ) : I --> C /\ ( z oF .^ G ) finSupp ( 1r ` S ) ) )
265	264	simpld 475	. . . . . . . . . 10 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) : I --> C )
266	20, 51, 31, 52, 263, 232, 236, 241	psrbagev1 19510	. . . . . . . . . . 11 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( w oF .^ G ) : I --> C /\ ( w oF .^ G ) finSupp ( 1r ` S ) ) )
267	266	simpld 475	. . . . . . . . . 10 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) : I --> C )
268	264	simprd 479	. . . . . . . . . 10 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) finSupp ( 1r ` S ) )
269	266	simprd 479	. . . . . . . . . 10 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) finSupp ( 1r ` S ) )
270	51, 52, 224, 263, 241, 265, 267, 268, 269	gsumadd 18323	. . . . . . . . 9 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsumg ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) = ( ( T gsumg ( z oF .^ G ) ) .x. ( T gsumg ( w oF .^ G ) ) ) )
271	262, 270	eqtrd 2656	. . . . . . . 8 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsumg ( ( z oF + w ) oF .^ G ) ) = ( ( T gsumg ( z oF .^ G ) ) .x. ( T gsumg ( w oF .^ G ) ) ) )
272	271	adantrl 752	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsumg ( ( z oF + w ) oF .^ G ) ) = ( ( T gsumg ( z oF .^ G ) ) .x. ( T gsumg ( w oF .^ G ) ) ) )
273	226, 272	oveq12d 6668	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsumg ( ( z oF + w ) oF .^ G ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsumg ( z oF .^ G ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) )
274	59	adantr 481	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> T e. CMnd )
275	68	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F : K --> C )
276	275, 216	ffvelrnd 6360	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( x ` z ) ) e. C )
277	275, 220	ffvelrnd 6360	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( y ` w ) ) e. C )
278	20, 51, 31, 52, 263, 228, 236, 241	psrbagev2 19511	. . . . . . . 8 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsumg ( z oF .^ G ) ) e. C )
279	278	adantrl 752	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsumg ( z oF .^ G ) ) e. C )
280	20, 51, 31, 52, 263, 232, 236, 241	psrbagev2 19511	. . . . . . . 8 |- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsumg ( w oF .^ G ) ) e. C )
281	280	adantrl 752	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsumg ( w oF .^ G ) ) e. C )
282	51, 224	cmn4 18212	. . . . . . 7 |- ( ( T e. CMnd /\ ( ( F ` ( x ` z ) ) e. C /\ ( F ` ( y ` w ) ) e. C ) /\ ( ( T gsumg ( z oF .^ G ) ) e. C /\ ( T gsumg ( w oF .^ G ) ) e. C ) ) -> ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsumg ( z oF .^ G ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsumg ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) )
283	274, 276, 277, 279, 281, 282	syl122anc 1335	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsumg ( z oF .^ G ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsumg ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) )
284	273, 283	eqtrd 2656	. . . . 5 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsumg ( ( z oF + w ) oF .^ G ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsumg ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) )
285	6	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> I e. _V )
286	7	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> R e. CRing )
287	13	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> S e. CRing )
288	36	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F e. ( R RingHom S ) )
289	38	adantr 481	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> G : I --> C )
290	20	psrbagaddcl 19370	. . . . . . 7 |- ( ( I e. _V /\ z e. D /\ w e. D ) -> ( z oF + w ) e. D )
291	285, 215, 219, 290	syl3anc 1326	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( z oF + w ) e. D )
292	9	adantr 481	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> R e. Ring )
293	22, 222	ringcl 18561	. . . . . . 7 |- ( ( R e. Ring /\ ( x ` z ) e. K /\ ( y ` w ) e. K ) -> ( ( x ` z ) ( .r ` R ) ( y ` w ) ) e. K )
294	292, 216, 220, 293	syl3anc 1326	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( x ` z ) ( .r ` R ) ( y ` w ) ) e. K )
295	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 291, 294	evlslem3 19514	. . . . 5 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = ( z oF + w ) , ( ( x ` z ) ( .r ` R ) ( y ` w ) ) , ( 0g ` R ) ) ) ) = ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsumg ( ( z oF + w ) oF .^ G ) ) ) )
296	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 215, 216	evlslem3 19514	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = z , ( x ` z ) , ( 0g ` R ) ) ) ) = ( ( F ` ( x ` z ) ) .x. ( T gsumg ( z oF .^ G ) ) ) )
297	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 219, 220	evlslem3 19514	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = w , ( y ` w ) , ( 0g ` R ) ) ) ) = ( ( F ` ( y ` w ) ) .x. ( T gsumg ( w oF .^ G ) ) ) )
298	296, 297	oveq12d 6668	. . . . 5 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( E ` ( v e. D |-> if ( v = z , ( x ` z ) , ( 0g ` R ) ) ) ) .x. ( E ` ( v e. D |-> if ( v = w , ( y ` w ) , ( 0g ` R ) ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsumg ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsumg ( w oF .^ G ) ) ) ) )
299	284, 295, 298	3eqtr4d 2666	. . . 4 |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = ( z oF + w ) , ( ( x ` z ) ( .r ` R ) ( y ` w ) ) , ( 0g ` R ) ) ) ) = ( ( E ` ( v e. D |-> if ( v = z , ( x ` z ) , ( 0g ` R ) ) ) ) .x. ( E ` ( v e. D |-> if ( v = w , ( y ` w ) , ( 0g ` R ) ) ) ) ) )
300	10, 1, 5, 21, 20, 6, 7, 13, 208, 299	evlslem2 19512	. . 3 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) )
301	1, 2, 3, 4, 5, 12, 15, 92, 300, 29, 93, 94, 116, 207	isrhmd 18729	. 2 |- ( ph -> E e. ( P RingHom S ) )
302		ovex 6678	. . . . . 6 |- ( S gsumg ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsumg ( b oF .^ G ) ) ) ) ) e. _V
303	302, 33	fnmpti 6022	. . . . 5 |- E Fn B
304	303	a1i 11	. . . 4 |- ( ph -> E Fn B )
305	22, 1	rhmf 18726	. . . . . 6 |- ( A e. ( R RingHom P ) -> A : K --> B )
306	86, 305	syl 17	. . . . 5 |- ( ph -> A : K --> B )
307	306	ffnd 6046	. . . 4 |- ( ph -> A Fn K )
308		frn 6053	. . . . 5 |- ( A : K --> B -> ran A C_ B )
309	306, 308	syl 17	. . . 4 |- ( ph -> ran A C_ B )
310		fnco 5999	. . . 4 |- ( ( E Fn B /\ A Fn K /\ ran A C_ B ) -> ( E o. A ) Fn K )
311	304, 307, 309, 310	syl3anc 1326	. . 3 |- ( ph -> ( E o. A ) Fn K )
312	68	ffnd 6046	. . 3 |- ( ph -> F Fn K )
313		fvco2 6273	. . . . 5 |- ( ( A Fn K /\ x e. K ) -> ( ( E o. A ) ` x ) = ( E ` ( A ` x ) ) )
314	307, 313	sylan 488	. . . 4 |- ( ( ph /\ x e. K ) -> ( ( E o. A ) ` x ) = ( E ` ( A ` x ) ) )
315	314, 73	eqtrd 2656	. . 3 |- ( ( ph /\ x e. K ) -> ( ( E o. A ) ` x ) = ( F ` x ) )
316	311, 312, 315	eqfnfvd 6314	. 2 |- ( ph -> ( E o. A ) = F )
317	10, 32, 1, 6, 9	mvrf2 19492	. . . . 5 |- ( ph -> V : I --> B )
318	317	ffnd 6046	. . . 4 |- ( ph -> V Fn I )
319		frn 6053	. . . . 5 |- ( V : I --> B -> ran V C_ B )
320	317, 319	syl 17	. . . 4 |- ( ph -> ran V C_ B )
321		fnco 5999	. . . 4 |- ( ( E Fn B /\ V Fn I /\ ran V C_ B ) -> ( E o. V ) Fn I )
322	304, 318, 320, 321	syl3anc 1326	. . 3 |- ( ph -> ( E o. V ) Fn I )
323		fvco2 6273	. . . . 5 |- ( ( V Fn I /\ x e. I ) -> ( ( E o. V ) ` x ) = ( E ` ( V ` x ) ) )
324	318, 323	sylan 488	. . . 4 |- ( ( ph /\ x e. I ) -> ( ( E o. V ) ` x ) = ( E ` ( V ` x ) ) )
325	6	adantr 481	. . . . . . 7 |- ( ( ph /\ x e. I ) -> I e. _V )
326	7	adantr 481	. . . . . . 7 |- ( ( ph /\ x e. I ) -> R e. CRing )
327		simpr 477	. . . . . . 7 |- ( ( ph /\ x e. I ) -> x e. I )
328	32, 20, 21, 75, 325, 326, 327	mvrval 19421	. . . . . 6 |- ( ( ph /\ x e. I ) -> ( V ` x ) = ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
329	328	fveq2d 6195	. . . . 5 |- ( ( ph /\ x e. I ) -> ( E ` ( V ` x ) ) = ( E ` ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
330	13	adantr 481	. . . . . 6 |- ( ( ph /\ x e. I ) -> S e. CRing )
331	36	adantr 481	. . . . . 6 |- ( ( ph /\ x e. I ) -> F e. ( R RingHom S ) )
332	38	adantr 481	. . . . . 6 |- ( ( ph /\ x e. I ) -> G : I --> C )
333	20	psrbagsn 19495	. . . . . . . 8 |- ( I e. _V -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D )
334	6, 333	syl 17	. . . . . . 7 |- ( ph -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D )
335	334	adantr 481	. . . . . 6 |- ( ( ph /\ x e. I ) -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D )
336	77	adantr 481	. . . . . 6 |- ( ( ph /\ x e. I ) -> ( 1r ` R ) e. K )
337	10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 325, 326, 330, 331, 332, 21, 335, 336	evlslem3 19514	. . . . 5 |- ( ( ph /\ x e. I ) -> ( E ` ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( ( F ` ( 1r ` R ) ) .x. ( T gsumg ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) )
338	91	adantr 481	. . . . . . 7 |- ( ( ph /\ x e. I ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
339		1nn0 11308	. . . . . . . . . . . . . 14 |- 1 e. NN0
340		0nn0 11307	. . . . . . . . . . . . . 14 |- 0 e. NN0
341	339, 340	keepel 4155	. . . . . . . . . . . . 13 |- if ( z = x , 1 , 0 ) e. NN0
342	341	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ z e. I ) -> if ( z = x , 1 , 0 ) e. NN0 )
343	38	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ph /\ z e. I ) -> ( G ` z ) e. C )
344		eqidd 2623	. . . . . . . . . . . 12 |- ( ph -> ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = x , 1 , 0 ) ) )
345	38	feqmptd 6249	. . . . . . . . . . . 12 |- ( ph -> G = ( z e. I |-> ( G ` z ) ) )
346	6, 342, 343, 344, 345	offval2 6914	. . . . . . . . . . 11 |- ( ph -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) )
347		oveq1 6657	. . . . . . . . . . . . . 14 |- ( 1 = if ( z = x , 1 , 0 ) -> ( 1 .^ ( G ` z ) ) = ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) )
348	347	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( 1 = if ( z = x , 1 , 0 ) -> ( ( 1 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) <-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
349		oveq1 6657	. . . . . . . . . . . . . 14 |- ( 0 = if ( z = x , 1 , 0 ) -> ( 0 .^ ( G ` z ) ) = ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) )
350	349	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( 0 = if ( z = x , 1 , 0 ) -> ( ( 0 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) <-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
351	343	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z e. I ) /\ z = x ) -> ( G ` z ) e. C )
352	51, 31	mulg1 17548	. . . . . . . . . . . . . . 15 |- ( ( G ` z ) e. C -> ( 1 .^ ( G ` z ) ) = ( G ` z ) )
353	351, 352	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z e. I ) /\ z = x ) -> ( 1 .^ ( G ` z ) ) = ( G ` z ) )
354		iftrue 4092	. . . . . . . . . . . . . . 15 |- ( z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` z ) )
355	354	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z e. I ) /\ z = x ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` z ) )
356	353, 355	eqtr4d 2659	. . . . . . . . . . . . 13 |- ( ( ( ph /\ z e. I ) /\ z = x ) -> ( 1 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
357	51, 52, 31	mulg0 17546	. . . . . . . . . . . . . . . 16 |- ( ( G ` z ) e. C -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) )
358	343, 357	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. I ) -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) )
359	358	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z e. I ) /\ -. z = x ) -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) )
360		iffalse 4095	. . . . . . . . . . . . . . 15 |- ( -. z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
361	360	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z e. I ) /\ -. z = x ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
362	359, 361	eqtr4d 2659	. . . . . . . . . . . . 13 |- ( ( ( ph /\ z e. I ) /\ -. z = x ) -> ( 0 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
363	348, 350, 356, 362	ifbothda 4123	. . . . . . . . . . . 12 |- ( ( ph /\ z e. I ) -> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
364	363	mpteq2dva 4744	. . . . . . . . . . 11 |- ( ph -> ( z e. I |-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
365	346, 364	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
366	365	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
367	366	oveq2d 6666	. . . . . . . 8 |- ( ( ph /\ x e. I ) -> ( T gsumg ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) = ( T gsumg ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) )
368	61	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. I ) -> T e. Mnd )
369	343	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. I ) /\ z e. I ) -> ( G ` z ) e. C )
370	29, 3	ringidcl 18568	. . . . . . . . . . . . 13 |- ( S e. Ring -> ( 1r ` S ) e. C )
371	15, 370	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( 1r ` S ) e. C )
372	371	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. I ) /\ z e. I ) -> ( 1r ` S ) e. C )
373	369, 372	ifcld 4131	. . . . . . . . . 10 |- ( ( ( ph /\ x e. I ) /\ z e. I ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) e. C )
374		eqid 2622	. . . . . . . . . 10 |- ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
375	373, 374	fmptd 6385	. . . . . . . . 9 |- ( ( ph /\ x e. I ) -> ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) : I --> C )
376		eldifn 3733	. . . . . . . . . . . . 13 |- ( z e. ( I \ { x } ) -> -. z e. { x } )
377		velsn 4193	. . . . . . . . . . . . 13 |- ( z e. { x } <-> z = x )
378	376, 377	sylnib 318	. . . . . . . . . . . 12 |- ( z e. ( I \ { x } ) -> -. z = x )
379	378, 360	syl 17	. . . . . . . . . . 11 |- ( z e. ( I \ { x } ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
380	379	adantl 482	. . . . . . . . . 10 |- ( ( ( ph /\ x e. I ) /\ z e. ( I \ { x } ) ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
381	380, 325	suppss2 7329	. . . . . . . . 9 |- ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) supp ( 1r ` S ) ) C_ { x } )
382	51, 52, 368, 325, 327, 375, 381	gsumpt 18361	. . . . . . . 8 |- ( ( ph /\ x e. I ) -> ( T gsumg ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) = ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) )
383		fveq2 6191	. . . . . . . . . . 11 |- ( z = x -> ( G ` z ) = ( G ` x ) )
384	354, 383	eqtrd 2656	. . . . . . . . . 10 |- ( z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` x ) )
385		fvex 6201	. . . . . . . . . 10 |- ( G ` x ) e. _V
386	384, 374, 385	fvmpt 6282	. . . . . . . . 9 |- ( x e. I -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) = ( G ` x ) )
387	386	adantl 482	. . . . . . . 8 |- ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) = ( G ` x ) )
388	367, 382, 387	3eqtrd 2660	. . . . . . 7 |- ( ( ph /\ x e. I ) -> ( T gsumg ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) = ( G ` x ) )
389	338, 388	oveq12d 6668	. . . . . 6 |- ( ( ph /\ x e. I ) -> ( ( F ` ( 1r ` R ) ) .x. ( T gsumg ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) = ( ( 1r ` S ) .x. ( G ` x ) ) )
390	29, 5, 3	ringlidm 18571	. . . . . . 7 |- ( ( S e. Ring /\ ( G ` x ) e. C ) -> ( ( 1r ` S ) .x. ( G ` x ) ) = ( G ` x ) )
391	15, 50, 390	syl2an2r 876	. . . . . 6 |- ( ( ph /\ x e. I ) -> ( ( 1r ` S ) .x. ( G ` x ) ) = ( G ` x ) )
392	389, 391	eqtrd 2656	. . . . 5 |- ( ( ph /\ x e. I ) -> ( ( F ` ( 1r ` R ) ) .x. ( T gsumg ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) = ( G ` x ) )
393	329, 337, 392	3eqtrd 2660	. . . 4 |- ( ( ph /\ x e. I ) -> ( E ` ( V ` x ) ) = ( G ` x ) )
394	324, 393	eqtrd 2656	. . 3 |- ( ( ph /\ x e. I ) -> ( ( E o. V ) ` x ) = ( G ` x ) )
395	322, 255, 394	eqfnfvd 6314	. 2 |- ( ph -> ( E o. V ) = G )
396	301, 316, 395	3jca 1242	1 |- ( ph -> ( E e. ( P RingHom S ) /\ ( E o. A ) = F /\ ( E o. V ) = G ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   ran crn 5115   "cima 5117   o. ccom 5118   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   ^m cmap 7857   Fincfn 7955   finSupp cfsupp 8275   0cc0 9936   1c1 9937   + caddc 9939   NNcn 11020   NN0cn0 11292   ZZcz 11377   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   0gc0g 16100   gsum_g cgsu 16101   Mndcmnd 17294   MndHom cmhm 17333   Grpcgrp 17422  ._gcmg 17540   GrpHom cghm 17657  CMndccmn 18193  mulGrpcmgp 18489   1rcur 18501   Ringcrg 18547   CRingccrg 18548   RingHom crh 18712  AssAlgcasa 19309  algSccascl 19311   mVar cmvr 19352   mPoly cmpl 19353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-tset 15960  df-0g 16102  df-gsum 16103  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-rnghom 18715  df-subrg 18778  df-lmod 18865  df-lss 18933  df-assa 19312  df-ascl 19314  df-psr 19356  df-mvr 19357  df-mpl 19358

This theorem is referenced by:  evlseu  19516