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 5 8 mplringd 
 |-  ( ph -> P e. Ring )
95 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
96 94 95 syl 
 |-  ( ph -> P e. CMnd )
97 96 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> P e. CMnd )
98 simprll 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> x e. Fin )
99 simprr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( x u. { z } ) C_ D )
100 99 unssad 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> x C_ D )
101 100 sselda 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ k e. x ) -> k e. D )
102 5 adantr 
 |-  ( ( ph /\ k e. D ) -> I e. W )
103 8 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
104 1 102 103 mpllmodd 
 |-  ( ( ph /\ k e. D ) -> P e. LMod )
105 11 ffvelcdmda 
 |-  ( ( ph /\ k e. D ) -> ( X ` k ) e. ( Base ` R ) )
106 1 5 8 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
107 106 adantr 
 |-  ( ( ph /\ k e. D ) -> R = ( Scalar ` P ) )
108 107 fveq2d 
 |-  ( ( ph /\ k e. D ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
109 105 108 eleqtrd 
 |-  ( ( ph /\ k e. D ) -> ( X ` k ) e. ( Base ` ( Scalar ` P ) ) )
110 simpr 
 |-  ( ( ph /\ k e. D ) -> k e. D )
111 1 6 3 4 2 102 103 110 mplmon 
 |-  ( ( ph /\ k e. D ) -> ( y e. D |-> if ( y = k , .1. , .0. ) ) e. B )
112 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
113 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
114 6 112 7 113 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 )
115 104 109 111 114 syl3anc 
 |-  ( ( ph /\ k e. D ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) e. B )
116 115 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 )
117 101 116 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 )
118 vex 
 |-  z e. _V
119 118 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> z e. _V )
120 simprlr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> -. z e. x )
121 1 5 8 mpllmodd 
 |-  ( ph -> P e. LMod )
122 121 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> P e. LMod )
123 11 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> X : D --> ( Base ` R ) )
124 99 unssbd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> { z } C_ D )
125 118 snss 
 |-  ( z e. D <-> { z } C_ D )
126 124 125 sylibr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> z e. D )
127 123 126 ffvelcdmd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( X ` z ) e. ( Base ` R ) )
128 106 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> R = ( Scalar ` P ) )
129 128 fveq2d 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
130 127 129 eleqtrd 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( X ` z ) e. ( Base ` ( Scalar ` P ) ) )
131 5 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> I e. W )
132 8 adantr 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> R e. Ring )
133 1 6 3 4 2 131 132 126 mplmon 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( y e. D |-> if ( y = z , .1. , .0. ) ) e. B )
134 6 112 7 113 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 )
135 122 130 133 134 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 )
136 fveq2 
 |-  ( k = z -> ( X ` k ) = ( X ` z ) )
137 equequ2 
 |-  ( k = z -> ( y = k <-> y = z ) )
138 137 ifbid 
 |-  ( k = z -> if ( y = k , .1. , .0. ) = if ( y = z , .1. , .0. ) )
139 138 mpteq2dv 
 |-  ( k = z -> ( y e. D |-> if ( y = k , .1. , .0. ) ) = ( y e. D |-> if ( y = z , .1. , .0. ) ) )
140 136 139 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. ) ) ) )
141 6 93 97 98 117 119 120 135 140 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. ) ) ) ) )
142 eqid 
 |-  ( +g ` R ) = ( +g ` R )
143 123 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( X ` y ) e. ( Base ` R ) )
144 10 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
145 8 144 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
146 145 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> .0. e. ( Base ` R ) )
147 143 146 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 ) )
148 147 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 ) )
149 fvex 
 |-  ( Base ` R ) e. _V
150 149 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 ) )
151 148 150 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 ) )
152 33 10 2 34 131 psrbas 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( Base ` ( I mPwSer R ) ) = ( ( Base ` R ) ^m D ) )
153 151 152 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 ) ) )
154 18 mptex 
 |-  ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) ) e. _V
155 funmpt 
 |-  Fun ( y e. D |-> if ( y e. x , ( X ` y ) , .0. ) )
156 154 155 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 )
157 156 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 ) )
158 eldifn 
 |-  ( y e. ( D \ x ) -> -. y e. x )
159 158 adantl 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. ( D \ x ) ) -> -. y e. x )
160 159 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. )
161 18 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> D e. _V )
162 160 161 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 )
163 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. )
164 157 98 162 163 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. )
165 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. ) )
166 153 164 165 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 )
167 1 6 142 93 166 135 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. ) ) ) ) )
168 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 )
169 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. ) ) )
170 eqid 
 |-  ( .r ` R ) = ( .r ` R )
171 1 7 10 6 170 2 127 133 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. ) ) ) )
172 127 adantr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> ( X ` z ) e. ( Base ` R ) )
173 10 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
174 173 144 ifcld 
 |-  ( R e. Ring -> if ( y = z , .1. , .0. ) e. ( Base ` R ) )
175 8 174 syl 
 |-  ( ph -> if ( y = z , .1. , .0. ) e. ( Base ` R ) )
176 175 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> if ( y = z , .1. , .0. ) e. ( Base ` R ) )
177 fconstmpt 
 |-  ( D X. { ( X ` z ) } ) = ( y e. D |-> ( X ` z ) )
178 177 a1i 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( D X. { ( X ` z ) } ) = ( y e. D |-> ( X ` z ) ) )
179 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. ) ) )
180 161 172 176 178 179 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. ) ) ) )
181 171 180 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. ) ) ) )
182 161 147 168 169 181 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. ) ) ) ) )
183 132 82 syl 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> R e. Grp )
184 10 142 3 grplid 
 |-  ( ( R e. Grp /\ ( X ` z ) e. ( Base ` R ) ) -> ( .0. ( +g ` R ) ( X ` z ) ) = ( X ` z ) )
185 183 127 184 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( .0. ( +g ` R ) ( X ` z ) ) = ( X ` z ) )
186 185 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 ) )
187 simpr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> y e. { z } )
188 velsn 
 |-  ( y e. { z } <-> y = z )
189 187 188 sylib 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> y = z )
190 189 fveq2d 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> ( X ` y ) = ( X ` z ) )
191 186 190 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 ) )
192 120 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> -. z e. x )
193 189 192 eqneltrd 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> -. y e. x )
194 193 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. )
195 189 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. )
196 195 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. ) )
197 10 170 4 ringridm 
 |-  ( ( R e. Ring /\ ( X ` z ) e. ( Base ` R ) ) -> ( ( X ` z ) ( .r ` R ) .1. ) = ( X ` z ) )
198 132 127 197 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) ( .r ` R ) .1. ) = ( X ` z ) )
199 198 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 ) )
200 196 199 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 ) )
201 194 200 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 ) ) )
202 elun2 
 |-  ( y e. { z } -> y e. ( x u. { z } ) )
203 202 adantl 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ y e. { z } ) -> y e. ( x u. { z } ) )
204 203 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 ) )
205 191 201 204 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. ) )
206 83 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) -> R e. Grp )
207 10 142 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. ) )
208 206 147 207 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. ) )
209 208 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. ) )
210 simpr 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> -. y e. { z } )
211 210 188 sylnib 
 |-  ( ( ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) /\ y e. D ) /\ -. y e. { z } ) -> -. y = z )
212 211 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. )
213 212 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. ) )
214 10 170 3 ringrz 
 |-  ( ( R e. Ring /\ ( X ` z ) e. ( Base ` R ) ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
215 132 127 214 syl2anc 
 |-  ( ( ph /\ ( ( x e. Fin /\ -. z e. x ) /\ ( x u. { z } ) C_ D ) ) -> ( ( X ` z ) ( .r ` R ) .0. ) = .0. )
216 215 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. )
217 213 216 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. )
218 217 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. ) )
219 elun 
 |-  ( y e. ( x u. { z } ) <-> ( y e. x \/ y e. { z } ) )
220 orcom 
 |-  ( ( y e. x \/ y e. { z } ) <-> ( y e. { z } \/ y e. x ) )
221 219 220 bitri 
 |-  ( y e. ( x u. { z } ) <-> ( y e. { z } \/ y e. x ) )
222 biorf 
 |-  ( -. y e. { z } -> ( y e. x <-> ( y e. { z } \/ y e. x ) ) )
223 221 222 bitr4id 
 |-  ( -. y e. { z } -> ( y e. ( x u. { z } ) <-> y e. x ) )
224 223 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 ) )
225 224 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. ) )
226 209 218 225 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. ) )
227 205 226 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. ) )
228 227 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. ) ) )
229 167 182 228 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. ) ) ) ) )
230 141 229 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. ) ) ) ) ) )
231 92 230 imbitrrid 
 |-  ( ( 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. ) ) ) )
232 231 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. ) ) ) ) )
233 232 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. ) ) ) ) )
234 91 233 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. ) ) ) ) )
235 234 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. ) ) ) ) ) )
236 235 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. ) ) ) ) ) )
237 54 63 72 81 87 236 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. ) ) ) ) )
238 38 237 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. ) ) ) )
239 32 238 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. ) ) )
240 30 239 eqtr4d 
 |-  ( ph -> X = ( P gsum ( k e. ( X supp .0. ) |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )
241 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. ) ) ) ) )
242 241 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. ) ) ) ) ) )
243 115 fmpttd 
 |-  ( ph -> ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) : D --> B )
244 11 16 19 21 suppssr 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( X ` k ) = .0. )
245 244 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. ) ) ) )
246 eldifi 
 |-  ( k e. ( D \ ( X supp .0. ) ) -> k e. D )
247 107 fveq2d 
 |-  ( ( ph /\ k e. D ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
248 3 247 eqtrid 
 |-  ( ( ph /\ k e. D ) -> .0. = ( 0g ` ( Scalar ` P ) ) )
249 248 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. ) ) ) )
250 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
251 6 112 7 250 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 ) )
252 104 111 251 syl2anc 
 |-  ( ( ph /\ k e. D ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
253 249 252 eqtrd 
 |-  ( ( ph /\ k e. D ) -> ( .0. .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
254 246 253 sylan2 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( .0. .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
255 245 254 eqtrd 
 |-  ( ( ph /\ k e. ( D \ ( X supp .0. ) ) ) -> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) = ( 0g ` P ) )
256 255 19 suppss2 
 |-  ( ph -> ( ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) supp ( 0g ` P ) ) C_ ( X supp .0. ) )
257 18 mptex 
 |-  ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) e. _V
258 funmpt 
 |-  Fun ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) )
259 fvex 
 |-  ( 0g ` P ) e. _V
260 257 258 259 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 )
261 260 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 ) )
262 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 ) )
263 261 38 256 262 syl12anc 
 |-  ( ph -> ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) finSupp ( 0g ` P ) )
264 6 44 96 19 243 256 263 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. ) ) ) ) ) )
265 242 264 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. ) ) ) ) ) )
266 240 265 eqtrd 
 |-  ( ph -> X = ( P gsum ( k e. D |-> ( ( X ` k ) .x. ( y e. D |-> if ( y = k , .1. , .0. ) ) ) ) ) )