Metamath Proof Explorer

Theorem mplcoe5

Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that R is a commutative ring (as in mplcoe2 ), it is sufficient that R is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses mplcoe1.p 
|- P = ( I mPoly R )
mplcoe1.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplcoe1.z 
|- .0. = ( 0g ` R )
mplcoe1.o 
|- .1. = ( 1r ` R )
mplcoe1.i 
|- ( ph -> I e. W )
mplcoe2.g 
|- G = ( mulGrp ` P )
mplcoe2.m 
|- .^ = ( .g ` G )
mplcoe2.v 
|- V = ( I mVar R )
mplcoe5.r 
|- ( ph -> R e. Ring )
mplcoe5.y 
|- ( ph -> Y e. D )
mplcoe5.c 
|- ( ph -> A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
Assertion mplcoe5 
|- ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( G gsum ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p 
 |-  P = ( I mPoly R )
2 mplcoe1.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplcoe1.z 
 |-  .0. = ( 0g ` R )
4 mplcoe1.o 
 |-  .1. = ( 1r ` R )
5 mplcoe1.i 
 |-  ( ph -> I e. W )
6 mplcoe2.g 
 |-  G = ( mulGrp ` P )
7 mplcoe2.m 
 |-  .^ = ( .g ` G )
8 mplcoe2.v 
 |-  V = ( I mVar R )
9 mplcoe5.r 
 |-  ( ph -> R e. Ring )
10 mplcoe5.y 
 |-  ( ph -> Y e. D )
11 mplcoe5.c 
 |-  ( ph -> A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
12 2 psrbag 
 |-  ( I e. W -> ( Y e. D <-> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) ) )
13 5 12 syl 
 |-  ( ph -> ( Y e. D <-> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) ) )
14 10 13 mpbid 
 |-  ( ph -> ( Y : I --> NN0 /\ ( `' Y " NN ) e. Fin ) )
15 14 simpld 
 |-  ( ph -> Y : I --> NN0 )
16 15 feqmptd 
 |-  ( ph -> Y = ( i e. I |-> ( Y ` i ) ) )
17 iftrue 
 |-  ( i e. ( `' Y " NN ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
18 17 adantl 
 |-  ( ( ( ph /\ i e. I ) /\ i e. ( `' Y " NN ) ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
19 eldif 
 |-  ( i e. ( I \ ( `' Y " NN ) ) <-> ( i e. I /\ -. i e. ( `' Y " NN ) ) )
20 frnnn0supp 
 |-  ( ( I e. W /\ Y : I --> NN0 ) -> ( Y supp 0 ) = ( `' Y " NN ) )
21 5 15 20 syl2anc 
 |-  ( ph -> ( Y supp 0 ) = ( `' Y " NN ) )
22 eqimss 
 |-  ( ( Y supp 0 ) = ( `' Y " NN ) -> ( Y supp 0 ) C_ ( `' Y " NN ) )
23 21 22 syl 
 |-  ( ph -> ( Y supp 0 ) C_ ( `' Y " NN ) )
24 c0ex 
 |-  0 e. _V
25 24 a1i 
 |-  ( ph -> 0 e. _V )
26 15 23 5 25 suppssr 
 |-  ( ( ph /\ i e. ( I \ ( `' Y " NN ) ) ) -> ( Y ` i ) = 0 )
27 26 ifeq2d 
 |-  ( ( ph /\ i e. ( I \ ( `' Y " NN ) ) ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , ( Y ` i ) ) = if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) )
28 ifid 
 |-  if ( i e. ( `' Y " NN ) , ( Y ` i ) , ( Y ` i ) ) = ( Y ` i )
29 27 28 eqtr3di 
 |-  ( ( ph /\ i e. ( I \ ( `' Y " NN ) ) ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
30 19 29 sylan2br 
 |-  ( ( ph /\ ( i e. I /\ -. i e. ( `' Y " NN ) ) ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
31 30 anassrs 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. ( `' Y " NN ) ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
32 18 31 pm2.61dan 
 |-  ( ( ph /\ i e. I ) -> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
33 32 mpteq2dva 
 |-  ( ph -> ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) = ( i e. I |-> ( Y ` i ) ) )
34 16 33 eqtr4d 
 |-  ( ph -> Y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) )
35 34 eqeq2d 
 |-  ( ph -> ( y = Y <-> y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) ) )
36 35 ifbid 
 |-  ( ph -> if ( y = Y , .1. , .0. ) = if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) )
37 36 mpteq2dv 
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) )
38 cnvimass 
 |-  ( `' Y " NN ) C_ dom Y
39 38 15 fssdm 
 |-  ( ph -> ( `' Y " NN ) C_ I )
40 14 simprd 
 |-  ( ph -> ( `' Y " NN ) e. Fin )
41 sseq1 
 |-  ( w = (/) -> ( w C_ I <-> (/) C_ I ) )
42 noel 
 |-  -. i e. (/)
43 eleq2 
 |-  ( w = (/) -> ( i e. w <-> i e. (/) ) )
44 42 43 mtbiri 
 |-  ( w = (/) -> -. i e. w )
45 44 iffalsed 
 |-  ( w = (/) -> if ( i e. w , ( Y ` i ) , 0 ) = 0 )
46 45 mpteq2dv 
 |-  ( w = (/) -> ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) = ( i e. I |-> 0 ) )
47 fconstmpt 
 |-  ( I X. { 0 } ) = ( i e. I |-> 0 )
48 46 47 eqtr4di 
 |-  ( w = (/) -> ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) = ( I X. { 0 } ) )
49 48 eqeq2d 
 |-  ( w = (/) -> ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) <-> y = ( I X. { 0 } ) ) )
50 49 ifbid 
 |-  ( w = (/) -> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) = if ( y = ( I X. { 0 } ) , .1. , .0. ) )
51 50 mpteq2dv 
 |-  ( w = (/) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) )
52 mpteq1 
 |-  ( w = (/) -> ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = ( k e. (/) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) )
53 mpt0 
 |-  ( k e. (/) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = (/)
54 52 53 eqtrdi 
 |-  ( w = (/) -> ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = (/) )
55 54 oveq2d 
 |-  ( w = (/) -> ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) = ( G gsum (/) ) )
56 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
57 6 56 ringidval 
 |-  ( 1r ` P ) = ( 0g ` G )
58 57 gsum0 
 |-  ( G gsum (/) ) = ( 1r ` P )
59 55 58 eqtrdi 
 |-  ( w = (/) -> ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) = ( 1r ` P ) )
60 51 59 eqeq12d 
 |-  ( w = (/) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 1r ` P ) ) )
61 41 60 imbi12d 
 |-  ( w = (/) -> ( ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) <-> ( (/) C_ I -> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 1r ` P ) ) ) )
62 61 imbi2d 
 |-  ( w = (/) -> ( ( ph -> ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) <-> ( ph -> ( (/) C_ I -> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 1r ` P ) ) ) ) )
63 sseq1 
 |-  ( w = x -> ( w C_ I <-> x C_ I ) )
64 eleq2 
 |-  ( w = x -> ( i e. w <-> i e. x ) )
65 64 ifbid 
 |-  ( w = x -> if ( i e. w , ( Y ` i ) , 0 ) = if ( i e. x , ( Y ` i ) , 0 ) )
66 65 mpteq2dv 
 |-  ( w = x -> ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) )
67 66 eqeq2d 
 |-  ( w = x -> ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) <-> y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) ) )
68 67 ifbid 
 |-  ( w = x -> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) = if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) )
69 68 mpteq2dv 
 |-  ( w = x -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) )
70 mpteq1 
 |-  ( w = x -> ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) )
71 70 oveq2d 
 |-  ( w = x -> ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
72 69 71 eqeq12d 
 |-  ( w = x -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) )
73 63 72 imbi12d 
 |-  ( w = x -> ( ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) <-> ( x C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
74 73 imbi2d 
 |-  ( w = x -> ( ( ph -> ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) <-> ( ph -> ( x C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) ) )
75 sseq1 
 |-  ( w = ( x u. { z } ) -> ( w C_ I <-> ( x u. { z } ) C_ I ) )
76 eleq2 
 |-  ( w = ( x u. { z } ) -> ( i e. w <-> i e. ( x u. { z } ) ) )
77 76 ifbid 
 |-  ( w = ( x u. { z } ) -> if ( i e. w , ( Y ` i ) , 0 ) = if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) )
78 77 mpteq2dv 
 |-  ( w = ( x u. { z } ) -> ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) )
79 78 eqeq2d 
 |-  ( w = ( x u. { z } ) -> ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) <-> y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) ) )
80 79 ifbid 
 |-  ( w = ( x u. { z } ) -> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) = if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) )
81 80 mpteq2dv 
 |-  ( w = ( x u. { z } ) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) )
82 mpteq1 
 |-  ( w = ( x u. { z } ) -> ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) )
83 82 oveq2d 
 |-  ( w = ( x u. { z } ) -> ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
84 81 83 eqeq12d 
 |-  ( w = ( x u. { z } ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) )
85 75 84 imbi12d 
 |-  ( w = ( x u. { z } ) -> ( ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) <-> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
86 85 imbi2d 
 |-  ( w = ( x u. { z } ) -> ( ( ph -> ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) <-> ( ph -> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) ) )
87 sseq1 
 |-  ( w = ( `' Y " NN ) -> ( w C_ I <-> ( `' Y " NN ) C_ I ) )
88 eleq2 
 |-  ( w = ( `' Y " NN ) -> ( i e. w <-> i e. ( `' Y " NN ) ) )
89 88 ifbid 
 |-  ( w = ( `' Y " NN ) -> if ( i e. w , ( Y ` i ) , 0 ) = if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) )
90 89 mpteq2dv 
 |-  ( w = ( `' Y " NN ) -> ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) )
91 90 eqeq2d 
 |-  ( w = ( `' Y " NN ) -> ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) <-> y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) ) )
92 91 ifbid 
 |-  ( w = ( `' Y " NN ) -> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) = if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) )
93 92 mpteq2dv 
 |-  ( w = ( `' Y " NN ) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) )
94 mpteq1 
 |-  ( w = ( `' Y " NN ) -> ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) )
95 94 oveq2d 
 |-  ( w = ( `' Y " NN ) -> ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
96 93 95 eqeq12d 
 |-  ( w = ( `' Y " NN ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) )
97 87 96 imbi12d 
 |-  ( w = ( `' Y " NN ) -> ( ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) <-> ( ( `' Y " NN ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
98 97 imbi2d 
 |-  ( w = ( `' Y " NN ) -> ( ( ph -> ( w C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. w , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. w |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) <-> ( ph -> ( ( `' Y " NN ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) ) )
99 1 2 3 4 56 5 9 mpl1 
 |-  ( ph -> ( 1r ` P ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) )
100 99 56 eqtr3di 
 |-  ( ph -> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 1r ` P ) )
101 100 a1d 
 |-  ( ph -> ( (/) C_ I -> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 1r ` P ) ) )
102 ssun1 
 |-  x C_ ( x u. { z } )
103 sstr2 
 |-  ( x C_ ( x u. { z } ) -> ( ( x u. { z } ) C_ I -> x C_ I ) )
104 102 103 ax-mp 
 |-  ( ( x u. { z } ) C_ I -> x C_ I )
105 104 imim1i 
 |-  ( ( x C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) -> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) )
106 oveq1 
 |-  ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) = ( ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) )
107 eqid 
 |-  ( Base ` P ) = ( Base ` P )
108 5 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> I e. W )
109 9 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> R e. Ring )
110 15 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> Y : I --> NN0 )
111 110 ffvelrnda 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) -> ( Y ` i ) e. NN0 )
112 0nn0 
 |-  0 e. NN0
113 ifcl 
 |-  ( ( ( Y ` i ) e. NN0 /\ 0 e. NN0 ) -> if ( i e. x , ( Y ` i ) , 0 ) e. NN0 )
114 111 112 113 sylancl 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) -> if ( i e. x , ( Y ` i ) , 0 ) e. NN0 )
115 114 fmpttd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) : I --> NN0 )
116 frnnn0supp 
 |-  ( ( I e. W /\ ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) : I --> NN0 ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) supp 0 ) = ( `' ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) " NN ) )
117 108 115 116 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) supp 0 ) = ( `' ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) " NN ) )
118 simprll 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> x e. Fin )
119 eldifn 
 |-  ( i e. ( I \ x ) -> -. i e. x )
120 119 adantl 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. ( I \ x ) ) -> -. i e. x )
121 120 iffalsed 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. ( I \ x ) ) -> if ( i e. x , ( Y ` i ) , 0 ) = 0 )
122 121 108 suppss2 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) supp 0 ) C_ x )
123 118 122 ssfid 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) supp 0 ) e. Fin )
124 117 123 eqeltrrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( `' ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) " NN ) e. Fin )
125 2 psrbag 
 |-  ( I e. W -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) e. D <-> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) : I --> NN0 /\ ( `' ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) " NN ) e. Fin ) ) )
126 108 125 syl 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) e. D <-> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) : I --> NN0 /\ ( `' ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) " NN ) e. Fin ) ) )
127 115 124 126 mpbir2and 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) e. D )
128 eqid 
 |-  ( .r ` P ) = ( .r ` P )
129 ssun2 
 |-  { z } C_ ( x u. { z } )
130 simprr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( x u. { z } ) C_ I )
131 129 130 sstrid 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> { z } C_ I )
132 vex 
 |-  z e. _V
133 132 snss 
 |-  ( z e. I <-> { z } C_ I )
134 131 133 sylibr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> z e. I )
135 110 134 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( Y ` z ) e. NN0 )
136 2 snifpsrbag 
 |-  ( ( I e. W /\ ( Y ` z ) e. NN0 ) -> ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) e. D )
137 108 135 136 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) e. D )
138 1 107 3 4 2 108 109 127 128 137 mplmonmul 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( y e. D |-> if ( y = ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) , .1. , .0. ) ) ) = ( y e. D |-> if ( y = ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) oF + ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) ) , .1. , .0. ) ) )
139 1 2 3 4 108 6 7 8 109 134 135 mplcoe3 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) , .1. , .0. ) ) = ( ( Y ` z ) .^ ( V ` z ) ) )
140 139 oveq2d 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( y e. D |-> if ( y = ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) , .1. , .0. ) ) ) = ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) )
141 135 adantr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) -> ( Y ` z ) e. NN0 )
142 ifcl 
 |-  ( ( ( Y ` z ) e. NN0 /\ 0 e. NN0 ) -> if ( i = z , ( Y ` z ) , 0 ) e. NN0 )
143 141 112 142 sylancl 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) -> if ( i = z , ( Y ` z ) , 0 ) e. NN0 )
144 eqidd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) )
145 eqidd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) = ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) )
146 108 114 143 144 145 offval2 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) oF + ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) ) = ( i e. I |-> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) ) )
147 111 adantr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> ( Y ` i ) e. NN0 )
148 147 nn0cnd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> ( Y ` i ) e. CC )
149 148 addid2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> ( 0 + ( Y ` i ) ) = ( Y ` i ) )
150 elsni 
 |-  ( i e. { z } -> i = z )
151 150 adantl 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> i = z )
152 simprlr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> -. z e. x )
153 152 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> -. z e. x )
154 151 153 eqneltrd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> -. i e. x )
155 154 iffalsed 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> if ( i e. x , ( Y ` i ) , 0 ) = 0 )
156 151 iftrued 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> if ( i = z , ( Y ` z ) , 0 ) = ( Y ` z ) )
157 151 fveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> ( Y ` i ) = ( Y ` z ) )
158 156 157 eqtr4d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> if ( i = z , ( Y ` z ) , 0 ) = ( Y ` i ) )
159 155 158 oveq12d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) = ( 0 + ( Y ` i ) ) )
160 simpr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> i e. { z } )
161 129 160 sselid 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> i e. ( x u. { z } ) )
162 161 iftrued 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) = ( Y ` i ) )
163 149 159 162 3eqtr4d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ i e. { z } ) -> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) = if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) )
164 114 adantr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> if ( i e. x , ( Y ` i ) , 0 ) e. NN0 )
165 164 nn0cnd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> if ( i e. x , ( Y ` i ) , 0 ) e. CC )
166 165 addid1d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> ( if ( i e. x , ( Y ` i ) , 0 ) + 0 ) = if ( i e. x , ( Y ` i ) , 0 ) )
167 simpr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> -. i e. { z } )
168 velsn 
 |-  ( i e. { z } <-> i = z )
169 167 168 sylnib 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> -. i = z )
170 169 iffalsed 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> if ( i = z , ( Y ` z ) , 0 ) = 0 )
171 170 oveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) = ( if ( i e. x , ( Y ` i ) , 0 ) + 0 ) )
172 elun 
 |-  ( i e. ( x u. { z } ) <-> ( i e. x \/ i e. { z } ) )
173 orcom 
 |-  ( ( i e. x \/ i e. { z } ) <-> ( i e. { z } \/ i e. x ) )
174 172 173 bitri 
 |-  ( i e. ( x u. { z } ) <-> ( i e. { z } \/ i e. x ) )
175 biorf 
 |-  ( -. i e. { z } -> ( i e. x <-> ( i e. { z } \/ i e. x ) ) )
176 174 175 bitr4id 
 |-  ( -. i e. { z } -> ( i e. ( x u. { z } ) <-> i e. x ) )
177 176 adantl 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> ( i e. ( x u. { z } ) <-> i e. x ) )
178 177 ifbid 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) = if ( i e. x , ( Y ` i ) , 0 ) )
179 166 171 178 3eqtr4d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) /\ -. i e. { z } ) -> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) = if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) )
180 163 179 pm2.61dan 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ i e. I ) -> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) = if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) )
181 180 mpteq2dva 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( i e. I |-> ( if ( i e. x , ( Y ` i ) , 0 ) + if ( i = z , ( Y ` z ) , 0 ) ) ) = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) )
182 146 181 eqtrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) oF + ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) ) = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) )
183 182 eqeq2d 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( y = ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) oF + ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) ) <-> y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) ) )
184 183 ifbid 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> if ( y = ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) oF + ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) ) , .1. , .0. ) = if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) )
185 184 mpteq2dv 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( y e. D |-> if ( y = ( ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) oF + ( i e. I |-> if ( i = z , ( Y ` z ) , 0 ) ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) )
186 138 140 185 3eqtr3rd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) )
187 6 107 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
188 6 128 mgpplusg 
 |-  ( .r ` P ) = ( +g ` G )
189 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
190 eqid 
 |-  ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) = ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) )
191 1 mplring 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. Ring )
192 5 9 191 syl2anc 
 |-  ( ph -> P e. Ring )
193 6 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
194 192 193 syl 
 |-  ( ph -> G e. Mnd )
195 194 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> G e. Mnd )
196 10 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> Y e. D )
197 fveq2 
 |-  ( x = a -> ( V ` x ) = ( V ` a ) )
198 197 oveq2d 
 |-  ( x = a -> ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` y ) ( +g ` G ) ( V ` a ) ) )
199 197 oveq1d 
 |-  ( x = a -> ( ( V ` x ) ( +g ` G ) ( V ` y ) ) = ( ( V ` a ) ( +g ` G ) ( V ` y ) ) )
200 198 199 eqeq12d 
 |-  ( x = a -> ( ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) <-> ( ( V ` y ) ( +g ` G ) ( V ` a ) ) = ( ( V ` a ) ( +g ` G ) ( V ` y ) ) ) )
201 fveq2 
 |-  ( y = b -> ( V ` y ) = ( V ` b ) )
202 201 oveq1d 
 |-  ( y = b -> ( ( V ` y ) ( +g ` G ) ( V ` a ) ) = ( ( V ` b ) ( +g ` G ) ( V ` a ) ) )
203 201 oveq2d 
 |-  ( y = b -> ( ( V ` a ) ( +g ` G ) ( V ` y ) ) = ( ( V ` a ) ( +g ` G ) ( V ` b ) ) )
204 202 203 eqeq12d 
 |-  ( y = b -> ( ( ( V ` y ) ( +g ` G ) ( V ` a ) ) = ( ( V ` a ) ( +g ` G ) ( V ` y ) ) <-> ( ( V ` b ) ( +g ` G ) ( V ` a ) ) = ( ( V ` a ) ( +g ` G ) ( V ` b ) ) ) )
205 200 204 cbvral2vw 
 |-  ( A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) <-> A. a e. I A. b e. I ( ( V ` b ) ( +g ` G ) ( V ` a ) ) = ( ( V ` a ) ( +g ` G ) ( V ` b ) ) )
206 11 205 sylib 
 |-  ( ph -> A. a e. I A. b e. I ( ( V ` b ) ( +g ` G ) ( V ` a ) ) = ( ( V ` a ) ( +g ` G ) ( V ` b ) ) )
207 206 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> A. a e. I A. b e. I ( ( V ` b ) ( +g ` G ) ( V ` a ) ) = ( ( V ` a ) ( +g ` G ) ( V ` b ) ) )
208 1 2 3 4 108 6 7 8 109 196 207 130 mplcoe5lem 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ran ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
209 102 130 sstrid 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> x C_ I )
210 209 sselda 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ k e. x ) -> k e. I )
211 194 adantr 
 |-  ( ( ph /\ k e. I ) -> G e. Mnd )
212 15 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( Y ` k ) e. NN0 )
213 5 adantr 
 |-  ( ( ph /\ k e. I ) -> I e. W )
214 9 adantr 
 |-  ( ( ph /\ k e. I ) -> R e. Ring )
215 simpr 
 |-  ( ( ph /\ k e. I ) -> k e. I )
216 1 8 107 213 214 215 mvrcl 
 |-  ( ( ph /\ k e. I ) -> ( V ` k ) e. ( Base ` P ) )
217 187 7 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( Y ` k ) e. NN0 /\ ( V ` k ) e. ( Base ` P ) ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` P ) )
218 211 212 216 217 syl3anc 
 |-  ( ( ph /\ k e. I ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` P ) )
219 218 adantlr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` P ) )
220 210 219 syldan 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ k e. x ) -> ( ( Y ` k ) .^ ( V ` k ) ) e. ( Base ` P ) )
221 1 8 107 108 109 134 mvrcl 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( V ` z ) e. ( Base ` P ) )
222 187 7 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( Y ` z ) e. NN0 /\ ( V ` z ) e. ( Base ` P ) ) -> ( ( Y ` z ) .^ ( V ` z ) ) e. ( Base ` P ) )
223 195 135 221 222 syl3anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( Y ` z ) .^ ( V ` z ) ) e. ( Base ` P ) )
224 fveq2 
 |-  ( k = z -> ( Y ` k ) = ( Y ` z ) )
225 fveq2 
 |-  ( k = z -> ( V ` k ) = ( V ` z ) )
226 224 225 oveq12d 
 |-  ( k = z -> ( ( Y ` k ) .^ ( V ` k ) ) = ( ( Y ` z ) .^ ( V ` z ) ) )
227 226 adantl 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) /\ k = z ) -> ( ( Y ` k ) .^ ( V ` k ) ) = ( ( Y ` z ) .^ ( V ` z ) ) )
228 187 188 189 190 195 118 208 220 134 152 223 227 gsumzunsnd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) = ( ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) )
229 186 228 eqeq12d 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) <-> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) = ( ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ( .r ` P ) ( ( Y ` z ) .^ ( V ` z ) ) ) ) )
230 106 229 syl5ibr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ I ) ) -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) )
231 230 expr 
 |-  ( ( ph /\ ( x e. Fin /\ -. z e. x ) ) -> ( ( x u. { z } ) C_ I -> ( ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
232 231 a2d 
 |-  ( ( ph /\ ( x e. Fin /\ -. z e. x ) ) -> ( ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) -> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
233 105 232 syl5 
 |-  ( ( ph /\ ( x e. Fin /\ -. z e. x ) ) -> ( ( x C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) -> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
234 233 expcom 
 |-  ( ( x e. Fin /\ -. z e. x ) -> ( ph -> ( ( x C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) -> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) ) )
235 234 a2d 
 |-  ( ( x e. Fin /\ -. z e. x ) -> ( ( ph -> ( x C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. x , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. x |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) -> ( ph -> ( ( x u. { z } ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( x u. { z } ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( x u. { z } ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) ) )
236 62 74 86 98 101 235 findcard2s 
 |-  ( ( `' Y " NN ) e. Fin -> ( ph -> ( ( `' Y " NN ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) ) )
237 40 236 mpcom 
 |-  ( ph -> ( ( `' Y " NN ) C_ I -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) ) )
238 39 237 mpd 
 |-  ( ph -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
239 39 resmptd 
 |-  ( ph -> ( ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) |` ( `' Y " NN ) ) = ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) )
240 239 oveq2d 
 |-  ( ph -> ( G gsum ( ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) |` ( `' Y " NN ) ) ) = ( G gsum ( k e. ( `' Y " NN ) |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
241 218 fmpttd 
 |-  ( ph -> ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) : I --> ( Base ` P ) )
242 ssidd 
 |-  ( ph -> I C_ I )
243 1 2 3 4 5 6 7 8 9 10 11 242 mplcoe5lem 
 |-  ( ph -> ran ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) C_ ( ( Cntz ` G ) ` ran ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
244 15 23 5 25 suppssr 
 |-  ( ( ph /\ k e. ( I \ ( `' Y " NN ) ) ) -> ( Y ` k ) = 0 )
245 244 oveq1d 
 |-  ( ( ph /\ k e. ( I \ ( `' Y " NN ) ) ) -> ( ( Y ` k ) .^ ( V ` k ) ) = ( 0 .^ ( V ` k ) ) )
246 eldifi 
 |-  ( k e. ( I \ ( `' Y " NN ) ) -> k e. I )
247 246 216 sylan2 
 |-  ( ( ph /\ k e. ( I \ ( `' Y " NN ) ) ) -> ( V ` k ) e. ( Base ` P ) )
248 187 57 7 mulg0 
 |-  ( ( V ` k ) e. ( Base ` P ) -> ( 0 .^ ( V ` k ) ) = ( 1r ` P ) )
249 247 248 syl 
 |-  ( ( ph /\ k e. ( I \ ( `' Y " NN ) ) ) -> ( 0 .^ ( V ` k ) ) = ( 1r ` P ) )
250 245 249 eqtrd 
 |-  ( ( ph /\ k e. ( I \ ( `' Y " NN ) ) ) -> ( ( Y ` k ) .^ ( V ` k ) ) = ( 1r ` P ) )
251 250 5 suppss2 
 |-  ( ph -> ( ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) supp ( 1r ` P ) ) C_ ( `' Y " NN ) )
252 5 mptexd 
 |-  ( ph -> ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) e. _V )
253 funmpt 
 |-  Fun ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) )
254 253 a1i 
 |-  ( ph -> Fun ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) )
255 fvexd 
 |-  ( ph -> ( 1r ` P ) e. _V )
256 suppssfifsupp 
 |-  ( ( ( ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) e. _V /\ Fun ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) /\ ( 1r ` P ) e. _V ) /\ ( ( `' Y " NN ) e. Fin /\ ( ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) supp ( 1r ` P ) ) C_ ( `' Y " NN ) ) ) -> ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) finSupp ( 1r ` P ) )
257 252 254 255 40 251 256 syl32anc 
 |-  ( ph -> ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) finSupp ( 1r ` P ) )
258 187 57 189 194 5 241 243 251 257 gsumzres 
 |-  ( ph -> ( G gsum ( ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) |` ( `' Y " NN ) ) ) = ( G gsum ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
259 238 240 258 3eqtr2d 
 |-  ( ph -> ( y e. D |-> if ( y = ( i e. I |-> if ( i e. ( `' Y " NN ) , ( Y ` i ) , 0 ) ) , .1. , .0. ) ) = ( G gsum ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )
260 37 259 eqtrd 
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( G gsum ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )