Metamath Proof Explorer

Theorem mplcoe1

Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015)

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 )
mplcoe1.b 
|- B = ( Base ` P )
mplcoe1.n 
|- .x. = ( .s ` P )
mplcoe1.r 
|- ( ph -> R e. Ring )
mplcoe1.x 
|- ( ph -> X e. B )
Assertion mplcoe1 
|- ( ph -> X = ( P gsum ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )

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 mplcoe1.b 
 |-  B = ( Base ` P )
7 mplcoe1.n 
 |-  .x. = ( .s ` P )
8 mplcoe1.r 
 |-  ( ph -> R e. Ring )
9 mplcoe1.x 
 |-  ( ph -> X e. B )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 1 10 6 2 9 mplelf 
 |-  ( ph -> X : D --> ( Base ` R ) )
12 11 feqmptd 
 |-  ( ph -> X = ( y e. D |-> ( X ` y ) ) )
13 iftrue 
 |-  ( y e. ( X supp .0. ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) = ( X ` y ) )
14 13 adantl 
 |-  ( ( ( ph /\ y e. D ) /\ y e. ( X supp .0. ) ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) = ( X ` y ) )
15 eldif 
 |-  ( y e. ( D \ ( X supp .0. ) ) <-> ( y e. D /\ -. y e. ( X supp .0. ) ) )
16 ssidd 
 |-  ( ph -> ( X supp .0. ) C_ ( X supp .0. ) )
17 ovex 
 |-  ( NN0 ^m I ) e. _V
18 2 17 rabex2 
 |-  D e. _V
19 18 a1i 
 |-  ( ph -> D e. _V )
20 3 fvexi 
 |-  .0. e. _V
21 20 a1i 
 |-  ( ph -> .0. e. _V )
22 11 16 19 21 suppssr 
 |-  ( ( ph /\ y e. ( D \ ( X supp .0. ) ) ) -> ( X ` y ) = .0. )
23 22 ifeq2d 
 |-  ( ( ph /\ y e. ( D \ ( X supp .0. ) ) ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , ( X ` y ) ) = if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) )
24 ifid 
 |-  if ( y e. ( X supp .0. ) , ( X ` y ) , ( X ` y ) ) = ( X ` y )
25 23 24 eqtr3di 
 |-  ( ( ph /\ y e. ( D \ ( X supp .0. ) ) ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) = ( X ` y ) )
26 15 25 sylan2br 
 |-  ( ( ph /\ ( y e. D /\ -. y e. ( X supp .0. ) ) ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) = ( X ` y ) )
27 26 anassrs 
 |-  ( ( ( ph /\ y e. D ) /\ -. y e. ( X supp .0. ) ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) = ( X ` y ) )
28 14 27 pm2.61dan 
 |-  ( ( ph /\ y e. D ) -> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) = ( X ` y ) )
29 28 mpteq2dva 
 |-  ( ph -> ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) = ( y e. D |-> ( X ` y ) ) )
30 12 29 eqtr4d 
 |-  ( ph -> X = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) )
31 suppssdm 
 |-  ( X supp .0. ) C_ dom X
32 31 11 fssdm 
 |-  ( ph -> ( X supp .0. ) C_ D )
33 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
34 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
35 1 33 34 3 6 mplelbas 
 |-  ( X e. B <-> ( X e. ( Base ` ( I mPwSer R ) ) /\ X finSupp .0. ) )
36 35 simprbi 
 |-  ( X e. B -> X finSupp .0. )
37 9 36 syl 
 |-  ( ph -> X finSupp .0. )
38 37 fsuppimpd 
 |-  ( ph -> ( X supp .0. ) e. Fin )
39 sseq1 
 |-  ( w = (/) -> ( w C_ D <-> (/) C_ D ) )
40 mpteq1 
 |-  ( w = (/) -> ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) = ( k e. (/) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) )
41 mpt0 
 |-  ( k e. (/) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) = (/)
42 40 41 eqtrdi 
 |-  ( w = (/) -> ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) = (/) )
43 42 oveq2d 
 |-  ( w = (/) -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( P gsum (/) ) )
44 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
45 44 gsum0 
 |-  ( P gsum (/) ) = ( 0g ` P )
46 43 45 eqtrdi 
 |-  ( w = (/) -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( 0g ` P ) )
47 noel 
 |-  -. y e. (/)
48 eleq2 
 |-  ( w = (/) -> ( y e. w <-> y e. (/) ) )
49 47 48 mtbiri 
 |-  ( w = (/) -> -. y e. w )
50 49 iffalsed 
 |-  ( w = (/) -> if ( y e. w , ( X ` y ) , .0. ) = .0. )
51 50 mpteq2dv 
 |-  ( w = (/) -> ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) = ( y e. D |-> .0. ) )
52 46 51 eqeq12d 
 |-  ( w = (/) -> ( ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) <-> ( 0g ` P ) = ( y e. D |-> .0. ) ) )
53 39 52 imbi12d 
 |-  ( w = (/) -> ( ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) <-> ( (/) C_ D -> ( 0g ` P ) = ( y e. D |-> .0. ) ) ) )
54 53 imbi2d 
 |-  ( w = (/) -> ( ( ph -> ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) ) <-> ( ph -> ( (/) C_ D -> ( 0g ` P ) = ( y e. D |-> .0. ) ) ) ) )
55 sseq1 
 |-  ( w = x -> ( w C_ D <-> x C_ D ) )
56 mpteq1 
 |-  ( w = x -> ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) = ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) )
57 56 oveq2d 
 |-  ( w = x -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
58 eleq2 
 |-  ( w = x -> ( y e. w <-> y e. x ) )
59 58 ifbid 
 |-  ( w = x -> if ( y e. w , ( X ` y ) , .0. ) = if ( y e. x , ( X ` y ) , .0. ) )
60 59 mpteq2dv 
 |-  ( w = x -> ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) )
61 57 60 eqeq12d 
 |-  ( w = x -> ( ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) <-> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) )
62 55 61 imbi12d 
 |-  ( w = x -> ( ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) <-> ( x C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) ) )
63 62 imbi2d 
 |-  ( w = x -> ( ( ph -> ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) ) <-> ( ph -> ( x C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) ) ) )
64 sseq1 
 |-  ( w = ( x u. { z } ) -> ( w C_ D <-> ( x u. { z } ) C_ D ) )
65 mpteq1 
 |-  ( w = ( x u. { z } ) -> ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) = ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) )
66 65 oveq2d 
 |-  ( w = ( x u. { z } ) -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
67 eleq2 
 |-  ( w = ( x u. { z } ) -> ( y e. w <-> y e. ( x u. { z } ) ) )
68 67 ifbid 
 |-  ( w = ( x u. { z } ) -> if ( y e. w , ( X ` y ) , .0. ) = if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) )
69 68 mpteq2dv 
 |-  ( w = ( x u. { z } ) -> ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) )
70 66 69 eqeq12d 
 |-  ( w = ( x u. { z } ) -> ( ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) <-> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) )
71 64 70 imbi12d 
 |-  ( w = ( x u. { z } ) -> ( ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) <-> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) )
72 71 imbi2d 
 |-  ( w = ( x u. { z } ) -> ( ( ph -> ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) ) <-> ( ph -> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) ) )
73 sseq1 
 |-  ( w = ( X supp .0. ) -> ( w C_ D <-> ( X supp .0. ) C_ D ) )
74 mpteq1 
 |-  ( w = ( X supp .0. ) -> ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) = ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) )
75 74 oveq2d 
 |-  ( w = ( X supp .0. ) -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
76 eleq2 
 |-  ( w = ( X supp .0. ) -> ( y e. w <-> y e. ( X supp .0. ) ) )
77 76 ifbid 
 |-  ( w = ( X supp .0. ) -> if ( y e. w , ( X ` y ) , .0. ) = if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) )
78 77 mpteq2dv 
 |-  ( w = ( X supp .0. ) -> ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) )
79 75 78 eqeq12d 
 |-  ( w = ( X supp .0. ) -> ( ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) <-> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) ) )
80 73 79 imbi12d 
 |-  ( w = ( X supp .0. ) -> ( ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) <-> ( ( X supp .0. ) C_ D -> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) ) ) )
81 80 imbi2d 
 |-  ( w = ( X supp .0. ) -> ( ( ph -> ( w C_ D -> ( P gsum ( k e. w |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. w , ( X ` y ) , .0. ) ) ) ) <-> ( ph -> ( ( X supp .0. ) C_ D -> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) ) ) ) )
82 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
83 8 82 syl 
 |-  ( ph -> R e. Grp )
84 1 2 3 44 5 83 mpl0 
 |-  ( ph -> ( 0g ` P ) = ( D X. { .0. } ) )
85 fconstmpt 
 |-  ( D X. { .0. } ) = ( y e. D |-> .0. )
86 84 85 eqtrdi 
 |-  ( ph -> ( 0g ` P ) = ( y e. D |-> .0. ) )
87 86 a1d 
 |-  ( ph -> ( (/) C_ D -> ( 0g ` P ) = ( y e. D |-> .0. ) ) )
88 ssun1 
 |-  x C_ ( x u. { z } )
89 sstr2 
 |-  ( x C_ ( x u. { z } ) -> ( ( x u. { z } ) C_ D -> x C_ D ) )
90 88 89 ax-mp 
 |-  ( ( x u. { z } ) C_ D -> x C_ D )
91 90 imim1i 
 |-  ( ( x C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) -> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) )
92 oveq1 
 |-  ( ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) -> ( ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) = ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) )
93 eqid 
 |-  ( +g ` P ) = ( +g ` P )
94 1 mplring 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. Ring )
95 5 8 94 syl2anc 
 |-  ( ph -> P e. Ring )
96 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
97 95 96 syl 
 |-  ( ph -> P e. CMnd )
98 97 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> P e. CMnd )
99 simprll 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> x e. Fin )
100 simprr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( x u. { z } ) C_ D )
101 100 unssad 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> x C_ D )
102 101 sselda 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ k e. x ) -> k e. D )
103 5 adantr 
 |-  ( ( ph /\ k e. D ) -> I e. W )
104 8 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
105 1 mpllmod 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. LMod )
106 103 104 105 syl2anc 
 |-  ( ( ph /\ k e. D ) -> P e. LMod )
107 11 ffvelrnda 
 |-  ( ( ph /\ k e. D ) -> ( X ` k ) e. ( Base ` R ) )
108 1 5 8 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
109 108 adantr 
 |-  ( ( ph /\ k e. D ) -> R = ( Scalar ` P ) )
110 109 fveq2d 
 |-  ( ( ph /\ k e. D ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
111 107 110 eleqtrd 
 |-  ( ( ph /\ k e. D ) -> ( X ` k ) e. ( Base ` ( Scalar ` P ) ) )
112 simpr 
 |-  ( ( ph /\ k e. D ) -> k e. D )
113 1 6 3 4 2 103 104 112 mplmon 
 |-  ( ( ph /\ k e. D ) -> ( y e. D |-> if ( y = k , .1. , .0. ) ) e. B )
114 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
115 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
116 6 114 7 115 lmodvscl 
 |-  ( ( P e. LMod /\ ( X ` k ) e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = k , .1. , .0. ) ) e. B ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) e. B )
117 106 111 113 116 syl3anc 
 |-  ( ( ph /\ k e. D ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) e. B )
118 117 adantlr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ k e. D ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) e. B )
119 102 118 syldan 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ k e. x ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) e. B )
120 vex 
 |-  z e. _V
121 120 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> z e. _V )
122 simprlr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> -. z e. x )
123 5 8 105 syl2anc 
 |-  ( ph -> P e. LMod )
124 123 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> P e. LMod )
125 11 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> X : D --> ( Base ` R ) )
126 100 unssbd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> { z } C_ D )
127 120 snss 
 |-  ( z e. D <-> { z } C_ D )
128 126 127 sylibr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> z e. D )
129 125 128 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( X ` z ) e. ( Base ` R ) )
130 108 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> R = ( Scalar ` P ) )
131 130 fveq2d 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
132 129 131 eleqtrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( X ` z ) e. ( Base ` ( Scalar ` P ) ) )
133 5 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> I e. W )
134 8 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> R e. Ring )
135 1 6 3 4 2 133 134 128 mplmon 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y = z , .1. , .0. ) ) e. B )
136 6 114 7 115 lmodvscl 
 |-  ( ( P e. LMod /\ ( X ` z ) e. ( Base ` ( Scalar ` P ) ) /\ ( y e. D |-> if ( y = z , .1. , .0. ) ) e. B ) -> ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) e. B )
137 124 132 135 136 syl3anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) e. B )
138 fveq2 
 |-  ( k = z -> ( X ` k ) = ( X ` z ) )
139 equequ2 
 |-  ( k = z -> ( y = k <-> y = z ) )
140 139 ifbid 
 |-  ( k = z -> if ( y = k , .1. , .0. ) = if ( y = z , .1. , .0. ) )
141 140 mpteq2dv 
 |-  ( k = z -> ( y e. D |-> if ( y = k , .1. , .0. ) ) = ( y e. D |-> if ( y = z , .1. , .0. ) ) )
142 138 141 oveq12d 
 |-  ( k = z -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) )
143 6 93 98 99 119 121 122 137 142 gsumunsn 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) )
144 eqid 
 |-  ( +g ` R ) = ( +g ` R )
145 125 ffvelrnda 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( X ` y ) e. ( Base ` R ) )
146 10 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
147 8 146 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
148 147 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> .0. e. ( Base ` R ) )
149 145 148 ifcld 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> if ( y e. x , ( X ` y ) , .0. ) e. ( Base ` R ) )
150 149 fmpttd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) : D --> ( Base ` R ) )
151 fvex 
 |-  ( Base ` R ) e. _V
152 151 18 elmap 
 |-  ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. ( ( Base ` R ) ^m D ) <-> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) : D --> ( Base ` R ) )
153 150 152 sylibr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. ( ( Base ` R ) ^m D ) )
154 33 10 2 34 133 psrbas 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( Base ` ( I mPwSer R ) ) = ( ( Base ` R ) ^m D ) )
155 153 154 eleqtrrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. ( Base ` ( I mPwSer R ) ) )
156 18 mptex 
 |-  ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. _V
157 funmpt 
 |-  Fun ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) )
158 156 157 20 3pm3.2i 
 |-  ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. _V /\ Fun ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) /\ .0. e. _V )
159 158 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. _V /\ Fun ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) /\ .0. e. _V ) )
160 eldifn 
 |-  ( y e. ( D \ x ) -> -. y e. x )
161 160 adantl 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. ( D \ x ) ) -> -. y e. x )
162 161 iffalsed 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. ( D \ x ) ) -> if ( y e. x , ( X ` y ) , .0. ) = .0. )
163 18 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> D e. _V )
164 162 163 suppss2 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) supp .0. ) C_ x )
165 suppssfifsupp 
 |-  ( ( ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. _V /\ Fun ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) /\ .0. e. _V ) /\ ( x e. Fin /\ ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) supp .0. ) C_ x ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) finSupp .0. )
166 159 99 164 165 syl12anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) finSupp .0. )
167 1 33 34 3 6 mplelbas 
 |-  ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. B <-> ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. ( Base ` ( I mPwSer R ) ) /\ ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) finSupp .0. ) )
168 155 166 167 sylanbrc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. B )
169 1 6 144 93 168 137 mpladd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) = ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) oF ( +g ` R ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) )
170 ovexd 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) e. _V )
171 eqidd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) )
172 eqid 
 |-  ( .r ` R ) = ( .r ` R )
173 1 7 10 6 172 2 129 135 mplvsca 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) = ( ( D X. { ( X ` z ) } ) oF ( .r ` R ) ( y e. D |-> if ( y = z , .1. , .0. ) ) ) )
174 129 adantr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( X ` z ) e. ( Base ` R ) )
175 10 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
176 175 146 ifcld 
 |-  ( R e. Ring -> if ( y = z , .1. , .0. ) e. ( Base ` R ) )
177 8 176 syl 
 |-  ( ph -> if ( y = z , .1. , .0. ) e. ( Base ` R ) )
178 177 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> if ( y = z , .1. , .0. ) e. ( Base ` R ) )
179 fconstmpt 
 |-  ( D X. { ( X ` z ) } ) = ( y e. D |-> ( X ` z ) )
180 179 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( D X. { ( X ` z ) } ) = ( y e. D |-> ( X ` z ) ) )
181 eqidd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y = z , .1. , .0. ) ) = ( y e. D |-> if ( y = z , .1. , .0. ) ) )
182 163 174 178 180 181 offval2 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( D X. { ( X ` z ) } ) oF ( .r ` R ) ( y e. D |-> if ( y = z , .1. , .0. ) ) ) = ( y e. D |-> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) )
183 173 182 eqtrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) = ( y e. D |-> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) )
184 163 149 170 171 183 offval2 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) oF ( +g ` R ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) = ( y e. D |-> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) ) )
185 134 82 syl 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> R e. Grp )
186 10 144 3 grplid 
 |-  ( ( R e. Grp /\ ( X ` z ) e. ( Base ` R ) ) -> ( .0. ( +g ` R ) ( X ` z ) ) = ( X ` z ) )
187 185 129 186 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( .0. ( +g ` R ) ( X ` z ) ) = ( X ` z ) )
188 187 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( .0. ( +g ` R ) ( X ` z ) ) = ( X ` z ) )
189 simpr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> y e. { z } )
190 velsn 
 |-  ( y e. { z } <-> y = z )
191 189 190 sylib 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> y = z )
192 191 fveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( X ` y ) = ( X ` z ) )
193 188 192 eqtr4d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( .0. ( +g ` R ) ( X ` z ) ) = ( X ` y ) )
194 122 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> -. z e. x )
195 191 194 eqneltrd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> -. y e. x )
196 195 iffalsed 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> if ( y e. x , ( X ` y ) , .0. ) = .0. )
197 191 iftrued 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> if ( y = z , .1. , .0. ) = .1. )
198 197 oveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) = ( ( X ` z ) ( .r ` R ) .1. ) )
199 10 172 4 ringridm 
 |-  ( ( R e. Ring /\ ( X ` z ) e. ( Base ` R ) ) -> ( ( X ` z ) ( .r ` R ) .1. ) = ( X ` z ) )
200 134 129 199 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) ( .r ` R ) .1. ) = ( X ` z ) )
201 200 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( ( X ` z ) ( .r ` R ) .1. ) = ( X ` z ) )
202 198 201 eqtrd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) = ( X ` z ) )
203 196 202 oveq12d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) = ( .0. ( +g ` R ) ( X ` z ) ) )
204 elun2 
 |-  ( y e. { z } -> y e. ( x u. { z } ) )
205 204 adantl 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> y e. ( x u. { z } ) )
206 205 iftrued 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) = ( X ` y ) )
207 193 203 206 3eqtr4d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) = if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) )
208 83 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> R e. Grp )
209 10 144 3 grprid 
 |-  ( ( R e. Grp /\ if ( y e. x , ( X ` y ) , .0. ) e. ( Base ` R ) ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) .0. ) = if ( y e. x , ( X ` y ) , .0. ) )
210 208 149 209 syl2anc 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) .0. ) = if ( y e. x , ( X ` y ) , .0. ) )
211 210 adantr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) .0. ) = if ( y e. x , ( X ` y ) , .0. ) )
212 simpr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> -. y e. { z } )
213 212 190 sylnib 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> -. y = z )
214 213 iffalsed 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> if ( y = z , .1. , .0. ) = .0. )
215 214 oveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) = ( ( X ` z ) ( .r ` R ) .0. ) )
216 10 172 3 ringrz 
 |-  ( ( R e. Ring /\ ( X ` z ) e. ( Base ` R ) ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
217 134 129 216 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
218 217 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
219 215 218 eqtrd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) = .0. )
220 219 oveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) = ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) .0. ) )
221 elun 
 |-  ( y e. ( x u. { z } ) <-> ( y e. x \/ y e. { z } ) )
222 orcom 
 |-  ( ( y e. x \/ y e. { z } ) <-> ( y e. { z } \/ y e. x ) )
223 221 222 bitri 
 |-  ( y e. ( x u. { z } ) <-> ( y e. { z } \/ y e. x ) )
224 biorf 
 |-  ( -. y e. { z } -> ( y e. x <-> ( y e. { z } \/ y e. x ) ) )
225 223 224 bitr4id 
 |-  ( -. y e. { z } -> ( y e. ( x u. { z } ) <-> y e. x ) )
226 225 adantl 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( y e. ( x u. { z } ) <-> y e. x ) )
227 226 ifbid 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) = if ( y e. x , ( X ` y ) , .0. ) )
228 211 220 227 3eqtr4d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) = if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) )
229 207 228 pm2.61dan 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) = if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) )
230 229 mpteq2dva 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> ( if ( y e. x , ( X ` y ) , .0. ) ( +g ` R ) ( ( X ` z ) ( .r ` R ) if ( y = z , .1. , .0. ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) )
231 169 184 230 3eqtrrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) = ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) )
232 143 231 eqeq12d 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) <-> ( ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) = ( ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ( +g ` P ) ( ( X ` z ) .x. ( y e. D |-> if ( y = z , .1. , .0. ) ) ) ) ) )
233 92 232 syl5ibr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) )
234 233 expr 
 |-  ( ( ph /\ ( x e. Fin /\ -. z e. x ) ) -> ( ( x u. { z } ) C_ D -> ( ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) )
235 234 a2d 
 |-  ( ( ph /\ ( x e. Fin /\ -. z e. x ) ) -> ( ( ( x u. { z } ) C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) -> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) )
236 91 235 syl5 
 |-  ( ( ph /\ ( x e. Fin /\ -. z e. x ) ) -> ( ( x C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) -> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) )
237 236 expcom 
 |-  ( ( x e. Fin /\ -. z e. x ) -> ( ph -> ( ( x C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) -> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) ) )
238 237 a2d 
 |-  ( ( x e. Fin /\ -. z e. x ) -> ( ( ph -> ( x C_ D -> ( P gsum ( k e. x |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) ) ) -> ( ph -> ( ( x u. { z } ) C_ D -> ( P gsum ( k e. ( x u. { z } ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( x u. { z } ) , ( X ` y ) , .0. ) ) ) ) ) )
239 54 63 72 81 87 238 findcard2s 
 |-  ( ( X supp .0. ) e. Fin -> ( ph -> ( ( X supp .0. ) C_ D -> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) ) ) )
240 38 239 mpcom 
 |-  ( ph -> ( ( X supp .0. ) C_ D -> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) ) )
241 32 240 mpd 
 |-  ( ph -> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( y e. D |-> if ( y e. ( X supp .0. ) , ( X ` y ) , .0. ) ) )
242 30 241 eqtr4d 
 |-  ( ph -> X = ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
243 32 resmptd 
 |-  ( ph -> ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) |` ( X supp .0. ) ) = ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) )
244 243 oveq2d 
 |-  ( ph -> ( P gsum ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) |` ( X supp .0. ) ) ) = ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
245 117 fmpttd 
 |-  ( ph -> ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) : D --> B )
246 11 16 19 21 suppssr 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( X ` k ) = .0. )
247 246 oveq1d 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( .0. .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) )
248 eldifi 
 |-  ( k e. ( D \ ( X supp .0. ) ) -> k e. D )
249 109 fveq2d 
 |-  ( ( ph /\ k e. D ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
250 3 249 eqtrid 
 |-  ( ( ph /\ k e. D ) -> .0. = ( 0g ` ( Scalar ` P ) ) )
251 250 oveq1d 
 |-  ( ( ph /\ k e. D ) -> ( .0. .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( ( 0g ` ( Scalar ` P ) ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) )
252 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
253 6 114 7 252 44 lmod0vs 
 |-  ( ( P e. LMod /\ ( y e. D |-> if ( y = k , .1. , .0. ) ) e. B ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
254 106 113 253 syl2anc 
 |-  ( ( ph /\ k e. D ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
255 251 254 eqtrd 
 |-  ( ( ph /\ k e. D ) -> ( .0. .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
256 248 255 sylan2 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( .0. .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
257 247 256 eqtrd 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
258 257 19 suppss2 
 |-  ( ph -> ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) supp ( 0g ` P ) ) C_ ( X supp .0. ) )
259 18 mptex 
 |-  ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) e. _V
260 funmpt 
 |-  Fun ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) )
261 fvex 
 |-  ( 0g ` P ) e. _V
262 259 260 261 3pm3.2i 
 |-  ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) e. _V /\ Fun ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) /\ ( 0g ` P ) e. _V )
263 262 a1i 
 |-  ( ph -> ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) e. _V /\ Fun ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) /\ ( 0g ` P ) e. _V ) )
264 suppssfifsupp 
 |-  ( ( ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) e. _V /\ Fun ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) /\ ( 0g ` P ) e. _V ) /\ ( ( X supp .0. ) e. Fin /\ ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) supp ( 0g ` P ) ) C_ ( X supp .0. ) ) ) -> ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) finSupp ( 0g ` P ) )
265 263 38 258 264 syl12anc 
 |-  ( ph -> ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) finSupp ( 0g ` P ) )
266 6 44 97 19 245 258 265 gsumres 
 |-  ( ph -> ( P gsum ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) |` ( X supp .0. ) ) ) = ( P gsum ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
267 244 266 eqtr3d 
 |-  ( ph -> ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) = ( P gsum ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
268 242 267 eqtrd 
 |-  ( ph -> X = ( P gsum ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )