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 = I mPoly R
evlselv.k ⊢ K = Base R
evlselv.b ⊢ B = Base P
evlselv.u ⊢ U = I ∖ J mPoly R
evlselv.t ⊢ T = J mPoly U
evlselv.l ⊢ L = algSc ⁡ U
evlselv.i ⊢ φ → I ∈ V
evlselv.r ⊢ φ → R ∈ CRing
evlselv.j ⊢ φ → J ⊆ I
evlselv.f ⊢ φ → F ∈ B
evlselv.a ⊢ φ → A ∈ K I
Assertion evlselv ⊢ φ → I ∖ J eval R ⁡ J eval U ⁡ I selectVars R ⁡ J ⁡ F ⁡ L ∘ A ↾ J ⁡ A ↾ I ∖ J = I eval R ⁡ F ⁡ A

Proof

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