Metamath Proof Explorer

Theorem evlselv

Description: Evaluating a selection of variable assignments, then evaluating the rest of the variables, is the same as evaluating with all assignments. (Contributed by SN, 10-Mar-2025)

Ref Expression
Hypotheses evlselv.p ⊢P=ImPolyR
evlselv.k ⊢K=BaseR
evlselv.b ⊢B=BaseP
evlselv.u ⊢U=I∖JmPolyR
evlselv.t ⊢T=JmPolyU
evlselv.l ⊢L=algSc⁡U
evlselv.i ⊢φ→I∈V
evlselv.r ⊢φ→R∈CRing
evlselv.j ⊢φ→J⊆I
evlselv.f ⊢φ→F∈B
evlselv.a ⊢φ→A∈KI
Assertion evlselv ⊢φ→I∖JevalR⁡JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡A↾I∖J=IevalR⁡F⁡A

Proof

Step Hyp Ref Expression
1 evlselv.p ⊢P=ImPolyR
2 evlselv.k ⊢K=BaseR
3 evlselv.b ⊢B=BaseP
4 evlselv.u ⊢U=I∖JmPolyR
5 evlselv.t ⊢T=JmPolyU
6 evlselv.l ⊢L=algSc⁡U
7 evlselv.i ⊢φ→I∈V
8 evlselv.r ⊢φ→R∈CRing
9 evlselv.j ⊢φ→J⊆I
10 evlselv.f ⊢φ→F∈B
11 evlselv.a ⊢φ→A∈KI
12 eqid ⊢BaseU=BaseU
13 eqid ⊢⋅U=⋅U
14 difssd ⊢φ→I∖J⊆I
15 7 14 ssexd ⊢φ→I∖J∈V
16 4 15 8 mplcrngd ⊢φ→U∈CRing
17 16 crngringd ⊢φ→U∈Ring
18 17 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→U∈Ring
19 eqid ⊢BaseT=BaseT
20 eqid ⊢g∈ℕ0J|g-1ℕ∈Fin=g∈ℕ0J|g-1ℕ∈Fin
21 1 3 4 5 19 7 8 9 10 selvcl ⊢φ→IselectVarsR⁡J⁡F∈BaseT
22 5 12 19 20 21 mplelf ⊢φ→IselectVarsR⁡J⁡F:g∈ℕ0J|g-1ℕ∈Fin⟶BaseU
23 22 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→IselectVarsR⁡J⁡F:g∈ℕ0J|g-1ℕ∈Fin⟶BaseU
24 23 ffvelcdmda ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e∈BaseU
25 eqid ⊢mulGrpU=mulGrpU
26 eqid ⊢⋅mulGrpU=⋅mulGrpU
27 7 9 ssexd ⊢φ→J∈V
28 27 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→J∈V
29 16 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→U∈CRing
30 fvexd ⊢φ→BaseU∈V
31 2 fvexi ⊢K∈V
32 31 a1i ⊢φ→K∈V
33 8 crngringd ⊢φ→R∈Ring
34 4 12 2 6 15 33 mplasclf ⊢φ→L:K⟶BaseU
35 30 32 34 elmapdd ⊢φ→L∈BaseUK
36 11 9 elmapssresd ⊢φ→A↾J∈KJ
37 35 36 mapcod ⊢φ→L∘A↾J∈BaseUJ
38 37 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→L∘A↾J∈BaseUJ
39 simpr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin
40 20 12 25 26 28 29 38 39 evlsvvvallem ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j∈BaseU
41 12 13 18 24 40 ringcld ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j∈BaseU
42 eqidd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
43 eqidd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→u∈BaseU⟼u⁡c=u∈BaseU⟼u⁡c
44 fveq1 ⊢u=IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j→u⁡c=IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c
45 41 42 43 44 fmptco ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→u∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c
46 34 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→L:K⟶BaseU
47 eqid ⊢mulGrpR=mulGrpR
48 47 2 mgpbas ⊢K=BasemulGrpR
49 eqid ⊢⋅mulGrpR=⋅mulGrpR
50 47 ringmgp ⊢R∈Ring→mulGrpR∈Mnd
51 33 50 syl ⊢φ→mulGrpR∈Mnd
52 51 ad3antrrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→mulGrpR∈Mnd
53 20 psrbagf ⊢e∈g∈ℕ0J|g-1ℕ∈Fin→e:J⟶ℕ0
54 53 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→e:J⟶ℕ0
55 54 ffvelcdmda ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→e⁡j∈ℕ0
56 elmapi ⊢A∈KI→A:I⟶K
57 11 56 syl ⊢φ→A:I⟶K
58 57 9 fssresd ⊢φ→A↾J:J⟶K
59 58 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→A↾J:J⟶K
60 59 ffvelcdmda ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→A↾J⁡j∈K
61 48 49 52 55 60 mulgnn0cld ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→e⁡j⋅mulGrpRA↾J⁡j∈K
62 46 61 cofmpt ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→L∘j∈J⟼e⁡j⋅mulGrpRA↾J⁡j=j∈J⟼L⁡e⁡j⋅mulGrpRA↾J⁡j
63 4 mplassa ⊢I∖J∈V∧R∈CRing→U∈AssAlg
64 15 8 63 syl2anc ⊢φ→U∈AssAlg
65 eqid ⊢Scalar⁡U=Scalar⁡U
66 6 65 asclrhm ⊢U∈AssAlg→L∈Scalar⁡URingHomU
67 64 66 syl ⊢φ→L∈Scalar⁡URingHomU
68 4 15 8 mplsca ⊢φ→R=Scalar⁡U
69 68 eqcomd ⊢φ→Scalar⁡U=R
70 69 oveq1d ⊢φ→Scalar⁡URingHomU=RRingHomU
71 67 70 eleqtrd ⊢φ→L∈RRingHomU
72 47 25 rhmmhm ⊢L∈RRingHomU→L∈mulGrpRMndHommulGrpU
73 71 72 syl ⊢φ→L∈mulGrpRMndHommulGrpU
74 73 ad3antrrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→L∈mulGrpRMndHommulGrpU
75 48 49 26 mhmmulg ⊢L∈mulGrpRMndHommulGrpU∧e⁡j∈ℕ0∧A↾J⁡j∈K→L⁡e⁡j⋅mulGrpRA↾J⁡j=e⁡j⋅mulGrpUL⁡A↾J⁡j
76 74 55 60 75 syl3anc ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→L⁡e⁡j⋅mulGrpRA↾J⁡j=e⁡j⋅mulGrpUL⁡A↾J⁡j
77 58 ad3antrrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→A↾J:J⟶K
78 simpr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→j∈J
79 77 78 fvco3d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→L∘A↾J⁡j=L⁡A↾J⁡j
80 79 oveq2d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→e⁡j⋅mulGrpUL∘A↾J⁡j=e⁡j⋅mulGrpUL⁡A↾J⁡j
81 76 80 eqtr4d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→L⁡e⁡j⋅mulGrpRA↾J⁡j=e⁡j⋅mulGrpUL∘A↾J⁡j
82 81 mpteq2dva ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼L⁡e⁡j⋅mulGrpRA↾J⁡j=j∈J⟼e⁡j⋅mulGrpUL∘A↾J⁡j
83 62 82 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→L∘j∈J⟼e⁡j⋅mulGrpRA↾J⁡j=j∈J⟼e⁡j⋅mulGrpUL∘A↾J⁡j
84 83 oveq2d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpUL∘j∈J⟼e⁡j⋅mulGrpRA↾J⁡j=∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
85 eqid ⊢BasemulGrpScalar⁡U=BasemulGrpScalar⁡U
86 eqid ⊢0mulGrpScalar⁡U=0mulGrpScalar⁡U
87 68 8 eqeltrrd ⊢φ→Scalar⁡U∈CRing
88 eqid ⊢mulGrpScalar⁡U=mulGrpScalar⁡U
89 88 crngmgp ⊢Scalar⁡U∈CRing→mulGrpScalar⁡U∈CMnd
90 87 89 syl ⊢φ→mulGrpScalar⁡U∈CMnd
91 90 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→mulGrpScalar⁡U∈CMnd
92 25 ringmgp ⊢U∈Ring→mulGrpU∈Mnd
93 17 92 syl ⊢φ→mulGrpU∈Mnd
94 93 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→mulGrpU∈Mnd
95 88 25 rhmmhm ⊢L∈Scalar⁡URingHomU→L∈mulGrpScalar⁡UMndHommulGrpU
96 67 95 syl ⊢φ→L∈mulGrpScalar⁡UMndHommulGrpU
97 96 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→L∈mulGrpScalar⁡UMndHommulGrpU
98 68 fveq2d ⊢φ→BaseR=BaseScalar⁡U
99 2 98 eqtrid ⊢φ→K=BaseScalar⁡U
100 99 ad3antrrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→K=BaseScalar⁡U
101 61 100 eleqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→e⁡j⋅mulGrpRA↾J⁡j∈BaseScalar⁡U
102 eqid ⊢BaseScalar⁡U=BaseScalar⁡U
103 88 102 mgpbas ⊢BaseScalar⁡U=BasemulGrpScalar⁡U
104 101 103 eleqtrdi ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧j∈J→e⁡j⋅mulGrpRA↾J⁡j∈BasemulGrpScalar⁡U
105 104 fmpttd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼e⁡j⋅mulGrpRA↾J⁡j:J⟶BasemulGrpScalar⁡U
106 27 mptexd ⊢φ→j∈J⟼e⁡j⋅mulGrpRA↾J⁡j∈V
107 106 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼e⁡j⋅mulGrpRA↾J⁡j∈V
108 fvexd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→0mulGrpR∈V
109 funmpt ⊢Fun⁡j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
110 109 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→Fun⁡j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
111 54 feqmptd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→e=j∈J⟼e⁡j
112 20 psrbagfsupp ⊢e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡e
113 112 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡e
114 111 113 eqbrtrrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡j∈J⟼e⁡j
115 ssidd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼e⁡jsupp0⊆j∈J⟼e⁡jsupp0
116 eqid ⊢0mulGrpR=0mulGrpR
117 48 116 49 mulg0 ⊢k∈K→0⋅mulGrpRk=0mulGrpR
118 117 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∧k∈K→0⋅mulGrpRk=0mulGrpR
119 0zd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→0∈ℤ
120 115 118 55 60 119 suppssov1 ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼e⁡j⋅mulGrpRA↾J⁡jsupp0mulGrpR⊆j∈J⟼e⁡jsupp0
121 107 108 110 114 120 fsuppsssuppgd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0mulGrpR⁡j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
122 eqid ⊢1R=1R
123 47 122 ringidval ⊢1R=0mulGrpR
124 121 123 breqtrrdi ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp1R⁡j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
125 68 fveq2d ⊢φ→1R=1Scalar⁡U
126 eqid ⊢1Scalar⁡U=1Scalar⁡U
127 88 126 ringidval ⊢1Scalar⁡U=0mulGrpScalar⁡U
128 125 127 eqtrdi ⊢φ→1R=0mulGrpScalar⁡U
129 128 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→1R=0mulGrpScalar⁡U
130 124 129 breqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0mulGrpScalar⁡U⁡j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
131 85 86 91 94 28 97 105 130 gsummhm ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpUL∘j∈J⟼e⁡j⋅mulGrpRA↾J⁡j=L⁡∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j
132 84 131 eqtr3d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=L⁡∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j
133 132 oveq2d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=IselectVarsR⁡J⁡F⁡e⋅UL⁡∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j
134 64 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→U∈AssAlg
135 101 fmpttd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼e⁡j⋅mulGrpRA↾J⁡j:J⟶BaseScalar⁡U
136 130 127 breqtrrdi ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→finSupp1Scalar⁡U⁡j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
137 103 127 91 28 135 136 gsumcl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j∈BaseScalar⁡U
138 eqid ⊢⋅U=⋅U
139 6 65 102 12 13 138 asclmul2 ⊢U∈AssAlg∧∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j∈BaseScalar⁡U∧IselectVarsR⁡J⁡F⁡e∈BaseU→IselectVarsR⁡J⁡F⁡e⋅UL⁡∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j=∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅UIselectVarsR⁡J⁡F⁡e
140 134 137 24 139 syl3anc ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⋅UL⁡∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j=∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅UIselectVarsR⁡J⁡F⁡e
141 133 140 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅UIselectVarsR⁡J⁡F⁡e
142 141 fveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c=∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅UIselectVarsR⁡J⁡F⁡e⁡c
143 eqid ⊢⋅R=⋅R
144 eqid ⊢f∈ℕ0I∖J|f-1ℕ∈Fin=f∈ℕ0I∖J|f-1ℕ∈Fin
145 99 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→K=BaseScalar⁡U
146 137 145 eleqtrrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j∈K
147 simplr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→c∈f∈ℕ0I∖J|f-1ℕ∈Fin
148 4 138 2 12 143 144 146 24 147 mplvscaval ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅UIselectVarsR⁡J⁡F⁡e⁡c=∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c
149 142 148 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c=∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c
150 149 mpteq2dva ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c=e∈g∈ℕ0J|g-1ℕ∈Fin⟼∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c
151 45 150 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→u∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=e∈g∈ℕ0J|g-1ℕ∈Fin⟼∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c
152 151 oveq2d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Ru∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=∑Re∈g∈ℕ0J|g-1ℕ∈Fin∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c
153 69 fveq2d ⊢φ→mulGrpScalar⁡U=mulGrpR
154 153 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→mulGrpScalar⁡U=mulGrpR
155 154 oveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j=∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
156 155 oveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c=∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c
157 8 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→R∈CRing
158 155 146 eqeltrrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j∈K
159 22 ffvelcdmda ⊢φ∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e∈BaseU
160 4 2 12 144 159 mplelf ⊢φ∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e:f∈ℕ0I∖J|f-1ℕ∈Fin⟶K
161 160 ffvelcdmda ⊢φ∧e∈g∈ℕ0J|g-1ℕ∈Fin∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⁡c∈K
162 161 an32s ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⁡c∈K
163 2 143 157 158 162 crngcomd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c=IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
164 156 163 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c=IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
165 164 mpteq2dva ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c=e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
166 165 oveq2d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Re∈g∈ℕ0J|g-1ℕ∈Fin∑mulGrpScalar⁡Uj∈Je⁡j⋅mulGrpRA↾J⁡j⋅RIselectVarsR⁡J⁡F⁡e⁡c=∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
167 152 166 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Ru∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
168 167 oveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Ru∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
169 eqid ⊢u∈BaseU⟼u⁡c=u∈BaseU⟼u⁡c
170 fveq1 ⊢u=∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j→u⁡c=∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c
171 eqid ⊢JevalU=JevalU
172 171 5 19 20 12 25 26 13 27 16 21 37 evlvvval ⊢φ→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J=∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
173 171 5 19 12 27 16 21 37 evlcl ⊢φ→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J∈BaseU
174 172 173 eqeltrrd ⊢φ→∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j∈BaseU
175 174 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j∈BaseU
176 fvexd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c∈V
177 169 170 175 176 fvmptd3 ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→u∈BaseU⟼u⁡c⁡∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c
178 eqid ⊢0U=0U
179 17 ringcmnd ⊢φ→U∈CMnd
180 179 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→U∈CMnd
181 8 crnggrpd ⊢φ→R∈Grp
182 181 grpmndd ⊢φ→R∈Mnd
183 182 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→R∈Mnd
184 ovex ⊢ℕ0J∈V
185 184 rabex ⊢g∈ℕ0J|g-1ℕ∈Fin∈V
186 185 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→g∈ℕ0J|g-1ℕ∈Fin∈V
187 15 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→I∖J∈V
188 181 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→R∈Grp
189 simpr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→c∈f∈ℕ0I∖J|f-1ℕ∈Fin
190 4 12 144 169 187 188 189 mplmapghm ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→u∈BaseU⟼u⁡c∈UGrpHomR
191 ghmmhm ⊢u∈BaseU⟼u⁡c∈UGrpHomR→u∈BaseU⟼u⁡c∈UMndHomR
192 190 191 syl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→u∈BaseU⟼u⁡c∈UMndHomR
193 41 fmpttd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j:g∈ℕ0J|g-1ℕ∈Fin⟶BaseU
194 27 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→J∈V
195 16 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→U∈CRing
196 21 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→IselectVarsR⁡J⁡F∈BaseT
197 37 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→L∘A↾J∈BaseUJ
198 20 5 19 12 25 26 13 194 195 196 197 evlvvvallem ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0U⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
199 12 178 180 183 186 192 193 198 gsummhm ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Ru∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j=u∈BaseU⟼u⁡c⁡∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
200 172 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J=∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
201 200 fveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c=∑Ue∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⁡c
202 177 199 201 3eqtr4rd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c=∑Ru∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j
203 202 oveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Ru∈BaseU⟼u⁡c∘e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⋅U∑mulGrpUj∈Je⁡j⋅mulGrpUL∘A↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
204 eqid ⊢0R=0R
205 33 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→R∈Ring
206 47 crngmgp ⊢R∈CRing→mulGrpR∈CMnd
207 8 206 syl ⊢φ→mulGrpR∈CMnd
208 207 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→mulGrpR∈CMnd
209 51 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧k∈I∖J→mulGrpR∈Mnd
210 144 psrbagf ⊢c∈f∈ℕ0I∖J|f-1ℕ∈Fin→c:I∖J⟶ℕ0
211 210 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→c:I∖J⟶ℕ0
212 211 ffvelcdmda ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧k∈I∖J→c⁡k∈ℕ0
213 57 14 fssresd ⊢φ→A↾I∖J:I∖J⟶K
214 213 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→A↾I∖J:I∖J⟶K
215 214 ffvelcdmda ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧k∈I∖J→A↾I∖J⁡k∈K
216 48 49 209 212 215 mulgnn0cld ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧k∈I∖J→c⁡k⋅mulGrpRA↾I∖J⁡k∈K
217 216 fmpttd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k:I∖J⟶K
218 15 mptexd ⊢φ→k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k∈V
219 218 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k∈V
220 fvexd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0mulGrpR∈V
221 funmpt ⊢Fun⁡k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k
222 221 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→Fun⁡k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k
223 211 feqmptd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→c=k∈I∖J⟼c⁡k
224 144 psrbagfsupp ⊢c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0⁡c
225 224 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0⁡c
226 223 225 eqbrtrrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0⁡k∈I∖J⟼c⁡k
227 ssidd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→k∈I∖J⟼c⁡ksupp0⊆k∈I∖J⟼c⁡ksupp0
228 48 116 49 mulg0 ⊢v∈K→0⋅mulGrpRv=0mulGrpR
229 228 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧v∈K→0⋅mulGrpRv=0mulGrpR
230 fvexd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧k∈I∖J→c⁡k∈V
231 0zd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0∈ℤ
232 227 229 230 215 231 suppssov1 ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡ksupp0mulGrpR⊆k∈I∖J⟼c⁡ksupp0
233 219 220 222 226 232 fsuppsssuppgd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0mulGrpR⁡k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k
234 48 116 208 187 217 233 gsumcl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k∈K
235 33 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→R∈Ring
236 2 143 235 162 158 ringcld ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j∈K
237 185 mptex ⊢e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j∈V
238 237 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j∈V
239 fvexd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0R∈V
240 funmpt ⊢Fun⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
241 240 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→Fun⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
242 185 mptex ⊢e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c∈V
243 242 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c∈V
244 funmpt ⊢Fun⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c
245 244 a1i ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→Fun⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c
246 5 19 178 21 16 mplelsfi ⊢φ→finSupp0U⁡IselectVarsR⁡J⁡F
247 246 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0U⁡IselectVarsR⁡J⁡F
248 ssidd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→IselectVarsR⁡J⁡Fsupp0U⊆IselectVarsR⁡J⁡Fsupp0U
249 fvexd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0U∈V
250 23 248 186 249 suppssr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∖supp0U⁡IselectVarsR⁡J⁡F→IselectVarsR⁡J⁡F⁡e=0U
251 250 fveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∖supp0U⁡IselectVarsR⁡J⁡F→IselectVarsR⁡J⁡F⁡e⁡c=0U⁡c
252 4 144 204 178 15 181 mpl0 ⊢φ→0U=f∈ℕ0I∖J|f-1ℕ∈Fin×0R
253 252 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0U=f∈ℕ0I∖J|f-1ℕ∈Fin×0R
254 253 fveq1d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0U⁡c=f∈ℕ0I∖J|f-1ℕ∈Fin×0R⁡c
255 fvex ⊢0R∈V
256 255 fvconst2 ⊢c∈f∈ℕ0I∖J|f-1ℕ∈Fin→f∈ℕ0I∖J|f-1ℕ∈Fin×0R⁡c=0R
257 256 adantl ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→f∈ℕ0I∖J|f-1ℕ∈Fin×0R⁡c=0R
258 254 257 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→0U⁡c=0R
259 258 adantr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∖supp0U⁡IselectVarsR⁡J⁡F→0U⁡c=0R
260 251 259 eqtrd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin∖supp0U⁡IselectVarsR⁡J⁡F→IselectVarsR⁡J⁡F⁡e⁡c=0R
261 260 186 suppss2 ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡csupp0R⊆IselectVarsR⁡J⁡Fsupp0U
262 243 239 245 247 261 fsuppsssuppgd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0R⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c
263 ssidd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡csupp0R⊆e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡csupp0R
264 33 ad2antrr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧v∈K→R∈Ring
265 simpr ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧v∈K→v∈K
266 2 143 204 264 265 ringlzd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧v∈K→0R⋅Rv=0R
267 263 266 162 158 239 suppssov1 ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡jsupp0R⊆e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡csupp0R
268 238 239 241 262 267 fsuppsssuppgd ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0R⁡e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
269 2 204 143 205 186 234 236 268 gsummulc1 ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
270 168 203 269 3eqtr4d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
271 fveq2 ⊢a=e→IselectVarsR⁡J⁡F⁡a=IselectVarsR⁡J⁡F⁡e
272 271 adantl ⊢b=c∧a=e→IselectVarsR⁡J⁡F⁡a=IselectVarsR⁡J⁡F⁡e
273 simpl ⊢b=c∧a=e→b=c
274 272 273 fveq12d ⊢b=c∧a=e→IselectVarsR⁡J⁡F⁡a⁡b=IselectVarsR⁡J⁡F⁡e⁡c
275 fveq1 ⊢a=e→a⁡j=e⁡j
276 275 adantl ⊢b=c∧a=e→a⁡j=e⁡j
277 276 oveq1d ⊢b=c∧a=e→a⁡j⋅mulGrpRA↾J⁡j=e⁡j⋅mulGrpRA↾J⁡j
278 277 mpteq2dv ⊢b=c∧a=e→j∈J⟼a⁡j⋅mulGrpRA↾J⁡j=j∈J⟼e⁡j⋅mulGrpRA↾J⁡j
279 278 oveq2d ⊢b=c∧a=e→∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j=∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
280 274 279 oveq12d ⊢b=c∧a=e→IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j=IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j
281 fveq1 ⊢b=c→b⁡k=c⁡k
282 281 adantr ⊢b=c∧a=e→b⁡k=c⁡k
283 282 oveq1d ⊢b=c∧a=e→b⁡k⋅mulGrpRA↾I∖J⁡k=c⁡k⋅mulGrpRA↾I∖J⁡k
284 283 mpteq2dv ⊢b=c∧a=e→k∈I∖J⟼b⁡k⋅mulGrpRA↾I∖J⁡k=k∈I∖J⟼c⁡k⋅mulGrpRA↾I∖J⁡k
285 284 oveq2d ⊢b=c∧a=e→∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k=∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
286 280 285 oveq12d ⊢b=c∧a=e→IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k=IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
287 eqid ⊢b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k=b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
288 ovex ⊢IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k∈V
289 286 287 288 ovmpoa ⊢c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→cb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke=IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
290 289 adantll ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin∧e∈g∈ℕ0J|g-1ℕ∈Fin→cb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke=IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
291 290 mpteq2dva ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→e∈g∈ℕ0J|g-1ℕ∈Fin⟼cb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke=e∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
292 291 oveq2d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→∑Re∈g∈ℕ0J|g-1ℕ∈Fincb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke=∑Re∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡e⁡c⋅R∑mulGrpRj∈Je⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
293 270 292 eqtr4d ⊢φ∧c∈f∈ℕ0I∖J|f-1ℕ∈Fin→JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Re∈g∈ℕ0J|g-1ℕ∈Fincb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke
294 293 mpteq2dva ⊢φ→c∈f∈ℕ0I∖J|f-1ℕ∈Fin⟼JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=c∈f∈ℕ0I∖J|f-1ℕ∈Fin⟼∑Re∈g∈ℕ0J|g-1ℕ∈Fincb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke
295 294 oveq2d ⊢φ→∑Rc∈f∈ℕ0I∖J|f-1ℕ∈FinJevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Rc∈f∈ℕ0I∖J|f-1ℕ∈Fin∑Re∈g∈ℕ0J|g-1ℕ∈Fincb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke
296 33 ringcmnd ⊢φ→R∈CMnd
297 ovex ⊢ℕ0I∈V
298 297 rabex ⊢h∈ℕ0I|h-1ℕ∈Fin∈V
299 298 a1i ⊢φ→h∈ℕ0I|h-1ℕ∈Fin∈V
300 33 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→R∈Ring
301 22 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F:g∈ℕ0J|g-1ℕ∈Fin⟶BaseU
302 eqid ⊢h∈ℕ0I|h-1ℕ∈Fin=h∈ℕ0I|h-1ℕ∈Fin
303 7 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→I∈V
304 9 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→J⊆I
305 simpr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d∈h∈ℕ0I|h-1ℕ∈Fin
306 302 20 303 304 305 psrbagres ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d↾J∈g∈ℕ0J|g-1ℕ∈Fin
307 301 306 ffvelcdmd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J∈BaseU
308 4 2 12 144 307 mplelf ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J:f∈ℕ0I∖J|f-1ℕ∈Fin⟶K
309 difssd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→I∖J⊆I
310 302 144 303 309 305 psrbagres ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d↾I∖J∈f∈ℕ0I∖J|f-1ℕ∈Fin
311 308 310 ffvelcdmd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J∈K
312 207 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→mulGrpR∈CMnd
313 27 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→J∈V
314 51 ad2antrr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→mulGrpR∈Mnd
315 302 psrbagf ⊢d∈h∈ℕ0I|h-1ℕ∈Fin→d:I⟶ℕ0
316 315 adantl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d:I⟶ℕ0
317 316 304 fssresd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d↾J:J⟶ℕ0
318 317 ffvelcdmda ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→d↾J⁡j∈ℕ0
319 58 ffvelcdmda ⊢φ∧j∈J→A↾J⁡j∈K
320 319 adantlr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→A↾J⁡j∈K
321 48 49 314 318 320 mulgnn0cld ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→d↾J⁡j⋅mulGrpRA↾J⁡j∈K
322 321 fmpttd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j:J⟶K
323 27 mptexd ⊢φ→j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j∈V
324 323 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j∈V
325 fvexd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→0mulGrpR∈V
326 funmpt ⊢Fun⁡j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j
327 326 a1i ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→Fun⁡j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j
328 302 psrbagfsupp ⊢d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0⁡d
329 328 adantl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0⁡d
330 0zd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→0∈ℤ
331 329 330 fsuppres ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0⁡d↾J
332 ssidd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d↾Jsupp0⊆d↾Jsupp0
333 317 332 313 330 suppssr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J∖supp0⁡d↾J→d↾J⁡j=0
334 333 oveq1d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J∖supp0⁡d↾J→d↾J⁡j⋅mulGrpRA↾J⁡j=0⋅mulGrpRA↾J⁡j
335 eldifi ⊢j∈J∖supp0⁡d↾J→j∈J
336 48 116 49 mulg0 ⊢A↾J⁡j∈K→0⋅mulGrpRA↾J⁡j=0mulGrpR
337 320 336 syl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→0⋅mulGrpRA↾J⁡j=0mulGrpR
338 335 337 sylan2 ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J∖supp0⁡d↾J→0⋅mulGrpRA↾J⁡j=0mulGrpR
339 334 338 eqtrd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J∖supp0⁡d↾J→d↾J⁡j⋅mulGrpRA↾J⁡j=0mulGrpR
340 339 313 suppss2 ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡jsupp0mulGrpR⊆d↾Jsupp0
341 324 325 327 331 340 fsuppsssuppgd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0mulGrpR⁡j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j
342 48 116 312 313 322 341 gsumcl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j∈K
343 2 143 300 311 342 ringcld ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j∈K
344 15 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→I∖J∈V
345 51 ad2antrr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→mulGrpR∈Mnd
346 316 309 fssresd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d↾I∖J:I∖J⟶ℕ0
347 346 ffvelcdmda ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→d↾I∖J⁡k∈ℕ0
348 213 ffvelcdmda ⊢φ∧k∈I∖J→A↾I∖J⁡k∈K
349 348 adantlr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→A↾I∖J⁡k∈K
350 48 49 345 347 349 mulgnn0cld ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∈K
351 350 fmpttd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k:I∖J⟶K
352 344 mptexd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∈V
353 funmpt ⊢Fun⁡k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
354 353 a1i ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→Fun⁡k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
355 329 330 fsuppres ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0⁡d↾I∖J
356 ssidd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d↾I∖Jsupp0⊆d↾I∖Jsupp0
357 346 356 344 330 suppssr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J∖supp0⁡d↾I∖J→d↾I∖J⁡k=0
358 357 oveq1d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J∖supp0⁡d↾I∖J→d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=0⋅mulGrpRA↾I∖J⁡k
359 eldifi ⊢k∈I∖J∖supp0⁡d↾I∖J→k∈I∖J
360 359 349 sylan2 ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J∖supp0⁡d↾I∖J→A↾I∖J⁡k∈K
361 48 116 49 mulg0 ⊢A↾I∖J⁡k∈K→0⋅mulGrpRA↾I∖J⁡k=0mulGrpR
362 360 361 syl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J∖supp0⁡d↾I∖J→0⋅mulGrpRA↾I∖J⁡k=0mulGrpR
363 358 362 eqtrd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J∖supp0⁡d↾I∖J→d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=0mulGrpR
364 363 344 suppss2 ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡ksupp0mulGrpR⊆d↾I∖Jsupp0
365 352 325 354 355 364 fsuppsssuppgd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0mulGrpR⁡k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
366 48 116 312 344 351 365 gsumcl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∈K
367 2 143 300 343 366 ringcld ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∈K
368 367 fmpttd ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k:h∈ℕ0I|h-1ℕ∈Fin⟶K
369 298 mptex ⊢d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∈V
370 369 a1i ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∈V
371 fvexd ⊢φ→0R∈V
372 funmpt ⊢Fun⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
373 372 a1i ⊢φ→Fun⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
374 298 mptex ⊢d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j∈V
375 374 a1i ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j∈V
376 funmpt ⊢Fun⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j
377 376 a1i ⊢φ→Fun⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j
378 8 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→R∈CRing
379 10 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→F∈B
380 302 1 3 303 378 304 379 305 selvvvval ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J=F⁡d
381 380 mpteq2dva ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J=d∈h∈ℕ0I|h-1ℕ∈Fin⟼F⁡d
382 eqid ⊢BaseR=BaseR
383 1 382 3 302 10 mplelf ⊢φ→F:h∈ℕ0I|h-1ℕ∈Fin⟶BaseR
384 383 feqmptd ⊢φ→F=d∈h∈ℕ0I|h-1ℕ∈Fin⟼F⁡d
385 1 3 204 10 8 mplelsfi ⊢φ→finSupp0R⁡F
386 384 385 eqbrtrrd ⊢φ→finSupp0R⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼F⁡d
387 381 386 eqbrtrd ⊢φ→finSupp0R⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J
388 ssidd ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖Jsupp0R⊆d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖Jsupp0R
389 33 adantr ⊢φ∧v∈K→R∈Ring
390 simpr ⊢φ∧v∈K→v∈K
391 2 143 204 389 390 ringlzd ⊢φ∧v∈K→0R⋅Rv=0R
392 fvexd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J∈V
393 388 391 392 342 371 suppssov1 ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡jsupp0R⊆d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖Jsupp0R
394 375 371 377 387 393 fsuppsssuppgd ⊢φ→finSupp0R⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j
395 ssidd ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡jsupp0R⊆d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡jsupp0R
396 ovexd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j∈V
397 395 391 396 366 371 suppssov1 ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡ksupp0R⊆d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡jsupp0R
398 370 371 373 394 397 fsuppsssuppgd ⊢φ→finSupp0R⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
399 eqid ⊢b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a=b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a
400 302 20 144 399 7 9 evlselvlem ⊢φ→b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a:f∈ℕ0I∖J|f-1ℕ∈Fin×g∈ℕ0J|g-1ℕ∈Fin⟶1-1 ontoh∈ℕ0I|h-1ℕ∈Fin
401 2 204 296 299 368 398 400 gsumf1o ⊢φ→∑Rd∈h∈ℕ0I|h-1ℕ∈FinIselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=∑Rd∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∘b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a
402 144 psrbagf ⊢b∈f∈ℕ0I∖J|f-1ℕ∈Fin→b:I∖J⟶ℕ0
403 402 ad2antrl ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b:I∖J⟶ℕ0
404 20 psrbagf ⊢a∈g∈ℕ0J|g-1ℕ∈Fin→a:J⟶ℕ0
405 404 ad2antll ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→a:J⟶ℕ0
406 disjdifr ⊢I∖J∩J=∅
407 406 a1i ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→I∖J∩J=∅
408 403 405 407 fun2d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a:I∖J∪J⟶ℕ0
409 undifr ⊢J⊆I↔I∖J∪J=I
410 9 409 sylib ⊢φ→I∖J∪J=I
411 410 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→I∖J∪J=I
412 411 feq2d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a:I∖J∪J⟶ℕ0↔b∪a:I⟶ℕ0
413 408 412 mpbid ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a:I⟶ℕ0
414 vex ⊢b∈V
415 vex ⊢a∈V
416 414 415 unex ⊢b∪a∈V
417 416 a1i ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a∈V
418 0zd ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→0∈ℤ
419 413 ffund ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→Fun⁡b∪a
420 144 psrbagfsupp ⊢b∈f∈ℕ0I∖J|f-1ℕ∈Fin→finSupp0⁡b
421 420 ad2antrl ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡b
422 20 psrbagfsupp ⊢a∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡a
423 422 ad2antll ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡a
424 421 423 fsuppun ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪asupp0∈Fin
425 417 418 419 424 isfsuppd ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡b∪a
426 fcdmnn0fsuppg ⊢b∪a∈V∧b∪a:I⟶ℕ0→finSupp0⁡b∪a↔b∪a-1ℕ∈Fin
427 417 413 426 syl2anc ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→finSupp0⁡b∪a↔b∪a-1ℕ∈Fin
428 425 427 mpbid ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a-1ℕ∈Fin
429 7 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→I∈V
430 302 psrbag ⊢I∈V→b∪a∈h∈ℕ0I|h-1ℕ∈Fin↔b∪a:I⟶ℕ0∧b∪a-1ℕ∈Fin
431 429 430 syl ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a∈h∈ℕ0I|h-1ℕ∈Fin↔b∪a:I⟶ℕ0∧b∪a-1ℕ∈Fin
432 413 428 431 mpbir2and ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a∈h∈ℕ0I|h-1ℕ∈Fin
433 eqidd ⊢φ→b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a=b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a
434 eqidd ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
435 reseq1 ⊢d=b∪a→d↾J=b∪a↾J
436 435 fveq2d ⊢d=b∪a→IselectVarsR⁡J⁡F⁡d↾J=IselectVarsR⁡J⁡F⁡b∪a↾J
437 reseq1 ⊢d=b∪a→d↾I∖J=b∪a↾I∖J
438 436 437 fveq12d ⊢d=b∪a→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J=IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J
439 435 fveq1d ⊢d=b∪a→d↾J⁡j=b∪a↾J⁡j
440 439 oveq1d ⊢d=b∪a→d↾J⁡j⋅mulGrpRA↾J⁡j=b∪a↾J⁡j⋅mulGrpRA↾J⁡j
441 440 mpteq2dv ⊢d=b∪a→j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j=j∈J⟼b∪a↾J⁡j⋅mulGrpRA↾J⁡j
442 441 oveq2d ⊢d=b∪a→∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j=∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j
443 438 442 oveq12d ⊢d=b∪a→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j=IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J⋅R∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j
444 437 fveq1d ⊢d=b∪a→d↾I∖J⁡k=b∪a↾I∖J⁡k
445 444 oveq1d ⊢d=b∪a→d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=b∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
446 445 mpteq2dv ⊢d=b∪a→k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=k∈I∖J⟼b∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
447 446 oveq2d ⊢d=b∪a→∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=∑mulGrpRk∈I∖Jb∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
448 443 447 oveq12d ⊢d=b∪a→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J⋅R∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
449 416 448 csbie ⊢⦋b∪a/d⦌IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J⋅R∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
450 402 ffnd ⊢b∈f∈ℕ0I∖J|f-1ℕ∈Fin→bFnI∖J
451 450 ad2antrl ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→bFnI∖J
452 405 ffnd ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→aFnJ
453 fnunres2 ⊢bFnI∖J∧aFnJ∧I∖J∩J=∅→b∪a↾J=a
454 451 452 407 453 syl3anc ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a↾J=a
455 454 fveq2d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡b∪a↾J=IselectVarsR⁡J⁡F⁡a
456 fnunres1 ⊢bFnI∖J∧aFnJ∧I∖J∩J=∅→b∪a↾I∖J=b
457 451 452 407 456 syl3anc ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a↾I∖J=b
458 455 457 fveq12d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J=IselectVarsR⁡J⁡F⁡a⁡b
459 454 fveq1d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a↾J⁡j=a⁡j
460 459 oveq1d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a↾J⁡j⋅mulGrpRA↾J⁡j=a⁡j⋅mulGrpRA↾J⁡j
461 460 mpteq2dv ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→j∈J⟼b∪a↾J⁡j⋅mulGrpRA↾J⁡j=j∈J⟼a⁡j⋅mulGrpRA↾J⁡j
462 461 oveq2d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j=∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j
463 458 462 oveq12d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J⋅R∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j=IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j
464 457 fveq1d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a↾I∖J⁡k=b⁡k
465 464 oveq1d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=b⁡k⋅mulGrpRA↾I∖J⁡k
466 465 mpteq2dv ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→k∈I∖J⟼b∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=k∈I∖J⟼b⁡k⋅mulGrpRA↾I∖J⁡k
467 466 oveq2d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpRk∈I∖Jb∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
468 463 467 oveq12d ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡b∪a↾J⁡b∪a↾I∖J⋅R∑mulGrpRj∈Jb∪a↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb∪a↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
469 449 468 eqtrid ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→⦋b∪a/d⦌IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
470 432 433 434 469 fmpocos ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∘b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a=b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
471 470 oveq2d ⊢φ→∑Rd∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∘b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a=∑Rb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
472 ovex ⊢ℕ0I∖J∈V
473 472 rabex ⊢f∈ℕ0I∖J|f-1ℕ∈Fin∈V
474 473 a1i ⊢φ→f∈ℕ0I∖J|f-1ℕ∈Fin∈V
475 185 a1i ⊢φ→g∈ℕ0J|g-1ℕ∈Fin∈V
476 33 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→R∈Ring
477 22 ffvelcdmda ⊢φ∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a∈BaseU
478 4 2 12 144 477 mplelf ⊢φ∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a:f∈ℕ0I∖J|f-1ℕ∈Fin⟶K
479 478 ffvelcdmda ⊢φ∧a∈g∈ℕ0J|g-1ℕ∈Fin∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a⁡b∈K
480 479 an32s ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a⁡b∈K
481 480 anasss ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a⁡b∈K
482 27 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→J∈V
483 8 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→R∈CRing
484 36 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→A↾J∈KJ
485 simprr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→a∈g∈ℕ0J|g-1ℕ∈Fin
486 20 2 47 49 482 483 484 485 evlsvvvallem ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j∈K
487 2 143 476 481 486 ringcld ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j∈K
488 15 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→I∖J∈V
489 11 14 elmapssresd ⊢φ→A↾I∖J∈KI∖J
490 489 adantr ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→A↾I∖J∈KI∖J
491 simprl ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→b∈f∈ℕ0I∖J|f-1ℕ∈Fin
492 144 2 47 49 488 483 490 491 evlsvvvallem ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k∈K
493 2 143 476 487 492 ringcld ⊢φ∧b∈f∈ℕ0I∖J|f-1ℕ∈Fin∧a∈g∈ℕ0J|g-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k∈K
494 493 ralrimivva ⊢φ→∀b∈f∈ℕ0I∖J|f-1ℕ∈Fin∀a∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k∈K
495 287 fmpo ⊢∀b∈f∈ℕ0I∖J|f-1ℕ∈Fin∀a∈g∈ℕ0J|g-1ℕ∈FinIselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k∈K↔b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k:f∈ℕ0I∖J|f-1ℕ∈Fin×g∈ℕ0J|g-1ℕ∈Fin⟶K
496 494 495 sylib ⊢φ→b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k:f∈ℕ0I∖J|f-1ℕ∈Fin×g∈ℕ0J|g-1ℕ∈Fin⟶K
497 f1of1 ⊢b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a:f∈ℕ0I∖J|f-1ℕ∈Fin×g∈ℕ0J|g-1ℕ∈Fin⟶1-1 ontoh∈ℕ0I|h-1ℕ∈Fin→b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a:f∈ℕ0I∖J|f-1ℕ∈Fin×g∈ℕ0J|g-1ℕ∈Fin⟶1-1h∈ℕ0I|h-1ℕ∈Fin
498 400 497 syl ⊢φ→b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a:f∈ℕ0I∖J|f-1ℕ∈Fin×g∈ℕ0J|g-1ℕ∈Fin⟶1-1h∈ℕ0I|h-1ℕ∈Fin
499 398 498 371 370 fsuppco ⊢φ→finSupp0R⁡d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k∘b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼b∪a
500 470 499 eqbrtrrd ⊢φ→finSupp0R⁡b∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k
501 2 204 296 474 475 496 500 gsumxp ⊢φ→∑Rb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡k=∑Rc∈f∈ℕ0I∖J|f-1ℕ∈Fin∑Re∈g∈ℕ0J|g-1ℕ∈Fincb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke
502 401 471 501 3eqtrd ⊢φ→∑Rd∈h∈ℕ0I|h-1ℕ∈FinIselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=∑Rc∈f∈ℕ0I∖J|f-1ℕ∈Fin∑Re∈g∈ℕ0J|g-1ℕ∈Fincb∈f∈ℕ0I∖J|f-1ℕ∈Fin,a∈g∈ℕ0J|g-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡a⁡b⋅R∑mulGrpRj∈Ja⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jb⁡k⋅mulGrpRA↾I∖J⁡ke
503 2 143 300 311 342 366 ringassd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
504 47 143 mgpplusg ⊢⋅R=+mulGrpR
505 51 ad2antrr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧i∈I→mulGrpR∈Mnd
506 316 ffvelcdmda ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧i∈I→d⁡i∈ℕ0
507 57 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→A:I⟶K
508 507 ffvelcdmda ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧i∈I→A⁡i∈K
509 48 49 505 506 508 mulgnn0cld ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧i∈I→d⁡i⋅mulGrpRA⁡i∈K
510 509 fmpttd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡i:I⟶K
511 7 mptexd ⊢φ→i∈I⟼d⁡i⋅mulGrpRA⁡i∈V
512 511 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡i∈V
513 funmpt ⊢Fun⁡i∈I⟼d⁡i⋅mulGrpRA⁡i
514 513 a1i ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→Fun⁡i∈I⟼d⁡i⋅mulGrpRA⁡i
515 316 feqmptd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→d=i∈I⟼d⁡i
516 515 329 eqbrtrrd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0⁡i∈I⟼d⁡i
517 ssidd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡isupp0⊆i∈I⟼d⁡isupp0
518 117 adantl ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈K→0⋅mulGrpRk=0mulGrpR
519 517 518 506 508 330 suppssov1 ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡isupp0mulGrpR⊆i∈I⟼d⁡isupp0
520 512 325 514 516 519 fsuppsssuppgd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→finSupp0mulGrpR⁡i∈I⟼d⁡i⋅mulGrpRA⁡i
521 disjdif ⊢J∩I∖J=∅
522 521 a1i ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→J∩I∖J=∅
523 undif ⊢J⊆I↔J∪I∖J=I
524 9 523 sylib ⊢φ→J∪I∖J=I
525 524 eqcomd ⊢φ→I=J∪I∖J
526 525 adantr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→I=J∪I∖J
527 48 116 504 312 303 510 520 522 526 gsumsplit ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i=∑mulGrpRi∈I⟼d⁡i⋅mulGrpRA⁡i↾J⋅R∑mulGrpRi∈I⟼d⁡i⋅mulGrpRA⁡i↾I∖J
528 304 resmptd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡i↾J=i∈J⟼d⁡i⋅mulGrpRA⁡i
529 fveq2 ⊢i=j→d⁡i=d⁡j
530 fveq2 ⊢i=j→A⁡i=A⁡j
531 529 530 oveq12d ⊢i=j→d⁡i⋅mulGrpRA⁡i=d⁡j⋅mulGrpRA⁡j
532 531 cbvmptv ⊢i∈J⟼d⁡i⋅mulGrpRA⁡i=j∈J⟼d⁡j⋅mulGrpRA⁡j
533 simpr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→j∈J
534 533 fvresd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→d↾J⁡j=d⁡j
535 533 fvresd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→A↾J⁡j=A⁡j
536 534 535 oveq12d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→d↾J⁡j⋅mulGrpRA↾J⁡j=d⁡j⋅mulGrpRA⁡j
537 536 eqcomd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧j∈J→d⁡j⋅mulGrpRA⁡j=d↾J⁡j⋅mulGrpRA↾J⁡j
538 537 mpteq2dva ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→j∈J⟼d⁡j⋅mulGrpRA⁡j=j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j
539 532 538 eqtrid ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈J⟼d⁡i⋅mulGrpRA⁡i=j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j
540 528 539 eqtrd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡i↾J=j∈J⟼d↾J⁡j⋅mulGrpRA↾J⁡j
541 540 oveq2d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRi∈I⟼d⁡i⋅mulGrpRA⁡i↾J=∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j
542 309 resmptd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡i↾I∖J=i∈I∖J⟼d⁡i⋅mulGrpRA⁡i
543 fveq2 ⊢i=k→d⁡i=d⁡k
544 fveq2 ⊢i=k→A⁡i=A⁡k
545 543 544 oveq12d ⊢i=k→d⁡i⋅mulGrpRA⁡i=d⁡k⋅mulGrpRA⁡k
546 545 cbvmptv ⊢i∈I∖J⟼d⁡i⋅mulGrpRA⁡i=k∈I∖J⟼d⁡k⋅mulGrpRA⁡k
547 simpr ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→k∈I∖J
548 547 fvresd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→d↾I∖J⁡k=d⁡k
549 547 fvresd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→A↾I∖J⁡k=A⁡k
550 548 549 oveq12d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=d⁡k⋅mulGrpRA⁡k
551 550 eqcomd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin∧k∈I∖J→d⁡k⋅mulGrpRA⁡k=d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
552 551 mpteq2dva ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→k∈I∖J⟼d⁡k⋅mulGrpRA⁡k=k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
553 546 552 eqtrid ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I∖J⟼d⁡i⋅mulGrpRA⁡i=k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
554 542 553 eqtrd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→i∈I⟼d⁡i⋅mulGrpRA⁡i↾I∖J=k∈I∖J⟼d↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
555 554 oveq2d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRi∈I⟼d⁡i⋅mulGrpRA⁡i↾I∖J=∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
556 541 555 oveq12d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRi∈I⟼d⁡i⋅mulGrpRA⁡i↾J⋅R∑mulGrpRi∈I⟼d⁡i⋅mulGrpRA⁡i↾I∖J=∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k
557 527 556 eqtr2d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
558 380 557 oveq12d ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=F⁡d⋅R∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
559 503 558 eqtrd ⊢φ∧d∈h∈ℕ0I|h-1ℕ∈Fin→IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=F⁡d⋅R∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
560 559 mpteq2dva ⊢φ→d∈h∈ℕ0I|h-1ℕ∈Fin⟼IselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=d∈h∈ℕ0I|h-1ℕ∈Fin⟼F⁡d⋅R∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
561 560 oveq2d ⊢φ→∑Rd∈h∈ℕ0I|h-1ℕ∈FinIselectVarsR⁡J⁡F⁡d↾J⁡d↾I∖J⋅R∑mulGrpRj∈Jd↾J⁡j⋅mulGrpRA↾J⁡j⋅R∑mulGrpRk∈I∖Jd↾I∖J⁡k⋅mulGrpRA↾I∖J⁡k=∑Rd∈h∈ℕ0I|h-1ℕ∈FinF⁡d⋅R∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
562 295 502 561 3eqtr2d ⊢φ→∑Rc∈f∈ℕ0I∖J|f-1ℕ∈FinJevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k=∑Rd∈h∈ℕ0I|h-1ℕ∈FinF⁡d⋅R∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
563 eqid ⊢I∖JevalR=I∖JevalR
564 563 4 12 144 2 47 49 143 15 8 173 489 evlvvval ⊢φ→I∖JevalR⁡JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡A↾I∖J=∑Rc∈f∈ℕ0I∖J|f-1ℕ∈FinJevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡c⋅R∑mulGrpRk∈I∖Jc⁡k⋅mulGrpRA↾I∖J⁡k
565 eqid ⊢IevalR=IevalR
566 565 1 3 302 2 47 49 143 7 8 10 11 evlvvval ⊢φ→IevalR⁡F⁡A=∑Rd∈h∈ℕ0I|h-1ℕ∈FinF⁡d⋅R∑mulGrpRi∈Id⁡i⋅mulGrpRA⁡i
567 562 564 566 3eqtr4d ⊢φ→I∖JevalR⁡JevalU⁡IselectVarsR⁡J⁡F⁡L∘A↾J⁡A↾I∖J=IevalR⁡F⁡A