Metamath Proof Explorer

Theorem elrgspnsubrunlem1

Description: Lemma for elrgspnsubrun , first direction. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses elrgspnsubrun.b ⊢ B = Base R
elrgspnsubrun.t ⊢ · ˙ = ⋅ R
elrgspnsubrun.z ⊢ 0 ˙ = 0 R
elrgspnsubrun.n ⊢ N = RingSpan ⁡ R
elrgspnsubrun.r ⊢ φ → R ∈ CRing
elrgspnsubrun.e ⊢ φ → E ∈ SubRing ⁡ R
elrgspnsubrun.f ⊢ φ → F ∈ SubRing ⁡ R
elrgspnsubrunlem1.p1 ⊢ φ → P : F ⟶ E
elrgspnsubrunlem1.p2 ⊢ φ → finSupp 0 ˙⁡ P
elrgspnsubrunlem1.x ⊢ φ → X = ∑ R e ∈ F P ⁡ e · ˙ e
elrgspnsubrunlem1.t ⊢ T = ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
Assertion elrgspnsubrunlem1 ⊢ φ → X ∈ N ⁡ E ∪ F

Proof

Step Hyp Ref Expression
1 elrgspnsubrun.b ⊢ B = Base R
2 elrgspnsubrun.t ⊢ · ˙ = ⋅ R
3 elrgspnsubrun.z ⊢ 0 ˙ = 0 R
4 elrgspnsubrun.n ⊢ N = RingSpan ⁡ R
5 elrgspnsubrun.r ⊢ φ → R ∈ CRing
6 elrgspnsubrun.e ⊢ φ → E ∈ SubRing ⁡ R
7 elrgspnsubrun.f ⊢ φ → F ∈ SubRing ⁡ R
8 elrgspnsubrunlem1.p1 ⊢ φ → P : F ⟶ E
9 elrgspnsubrunlem1.p2 ⊢ φ → finSupp 0 ˙⁡ P
10 elrgspnsubrunlem1.x ⊢ φ → X = ∑ R e ∈ F P ⁡ e · ˙ e
11 elrgspnsubrunlem1.t ⊢ T = ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
12 fveq1 ⊢ g = 𝟙 Word E ∪ F ⁡ T → g ⁡ w = 𝟙 Word E ∪ F ⁡ T ⁡ w
13 12 oveq1d ⊢ g = 𝟙 Word E ∪ F ⁡ T → g ⁡ w ⋅ R ∑ mulGrp R w = 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
14 13 mpteq2dv ⊢ g = 𝟙 Word E ∪ F ⁡ T → w ∈ Word E ∪ F ⟼ g ⁡ w ⋅ R ∑ mulGrp R w = w ∈ Word E ∪ F ⟼ 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
15 14 oveq2d ⊢ g = 𝟙 Word E ∪ F ⁡ T → ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w = ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
16 15 eqeq2d ⊢ g = 𝟙 Word E ∪ F ⁡ T → X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w ↔ X = ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
17 breq1 ⊢ h = 𝟙 Word E ∪ F ⁡ T → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ 𝟙 Word E ∪ F ⁡ T
18 zex ⊢ ℤ ∈ V
19 18 a1i ⊢ φ → ℤ ∈ V
20 6 7 unexd ⊢ φ → E ∪ F ∈ V
21 wrdexg ⊢ E ∪ F ∈ V → Word E ∪ F ∈ V
22 20 21 syl ⊢ φ → Word E ∪ F ∈ V
23 ssun1 ⊢ E ⊆ E ∪ F
24 8 adantr ⊢ φ ∧ f ∈ supp 0 ˙⁡ P → P : F ⟶ E
25 suppssdm ⊢ P supp 0 ˙ ⊆ dom ⁡ P
26 25 8 fssdm ⊢ φ → P supp 0 ˙ ⊆ F
27 26 sselda ⊢ φ ∧ f ∈ supp 0 ˙⁡ P → f ∈ F
28 24 27 ffvelcdmd ⊢ φ ∧ f ∈ supp 0 ˙⁡ P → P ⁡ f ∈ E
29 23 28 sselid ⊢ φ ∧ f ∈ supp 0 ˙⁡ P → P ⁡ f ∈ E ∪ F
30 ssun2 ⊢ F ⊆ E ∪ F
31 26 30 sstrdi ⊢ φ → P supp 0 ˙ ⊆ E ∪ F
32 31 sselda ⊢ φ ∧ f ∈ supp 0 ˙⁡ P → f ∈ E ∪ F
33 29 32 s2cld ⊢ φ ∧ f ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ f f ”⟩ ∈ Word E ∪ F
34 33 ralrimiva ⊢ φ → ∀ f ∈ supp 0 ˙⁡ P ⟨“ P ⁡ f f ”⟩ ∈ Word E ∪ F
35 eqid ⊢ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ = f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
36 35 rnmptss ⊢ ∀ f ∈ supp 0 ˙⁡ P ⟨“ P ⁡ f f ”⟩ ∈ Word E ∪ F → ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ ⊆ Word E ∪ F
37 34 36 syl ⊢ φ → ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ ⊆ Word E ∪ F
38 11 37 eqsstrid ⊢ φ → T ⊆ Word E ∪ F
39 indf ⊢ Word E ∪ F ∈ V ∧ T ⊆ Word E ∪ F → 𝟙 Word E ∪ F ⁡ T : Word E ∪ F ⟶ 0 1
40 22 38 39 syl2anc ⊢ φ → 𝟙 Word E ∪ F ⁡ T : Word E ∪ F ⟶ 0 1
41 0zd ⊢ φ → 0 ∈ ℤ
42 1zzd ⊢ φ → 1 ∈ ℤ
43 41 42 prssd ⊢ φ → 0 1 ⊆ ℤ
44 40 43 fssd ⊢ φ → 𝟙 Word E ∪ F ⁡ T : Word E ∪ F ⟶ ℤ
45 19 22 44 elmapdd ⊢ φ → 𝟙 Word E ∪ F ⁡ T ∈ ℤ Word E ∪ F
46 40 ffund ⊢ φ → Fun ⁡ 𝟙 Word E ∪ F ⁡ T
47 indsupp ⊢ Word E ∪ F ∈ V ∧ T ⊆ Word E ∪ F → 𝟙 Word E ∪ F ⁡ T supp 0 = T
48 22 38 47 syl2anc ⊢ φ → 𝟙 Word E ∪ F ⁡ T supp 0 = T
49 9 fsuppimpd ⊢ φ → P supp 0 ˙ ∈ Fin
50 mptfi ⊢ P supp 0 ˙ ∈ Fin → f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ ∈ Fin
51 rnfi ⊢ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ ∈ Fin → ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ ∈ Fin
52 49 50 51 3syl ⊢ φ → ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ ∈ Fin
53 11 52 eqeltrid ⊢ φ → T ∈ Fin
54 48 53 eqeltrd ⊢ φ → 𝟙 Word E ∪ F ⁡ T supp 0 ∈ Fin
55 45 41 46 54 isfsuppd ⊢ φ → finSupp 0 ⁡ 𝟙 Word E ∪ F ⁡ T
56 17 45 55 elrabd ⊢ φ → 𝟙 Word E ∪ F ⁡ T ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h
57 5 crngringd ⊢ φ → R ∈ Ring
58 57 ringcmnd ⊢ φ → R ∈ CMnd
59 8 ffnd ⊢ φ → P Fn F
60 59 adantr ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → P Fn F
61 7 adantr ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → F ∈ SubRing ⁡ R
62 3 fvexi ⊢ 0 ˙ ∈ V
63 62 a1i ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → 0 ˙ ∈ V
64 simpr ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → e ∈ F ∖ supp 0 ˙⁡ P
65 60 61 63 64 fvdifsupp ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → P ⁡ e = 0 ˙
66 65 oveq1d ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → P ⁡ e · ˙ e = 0 ˙ · ˙ e
67 57 adantr ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → R ∈ Ring
68 1 subrgss ⊢ F ∈ SubRing ⁡ R → F ⊆ B
69 7 68 syl ⊢ φ → F ⊆ B
70 69 ssdifssd ⊢ φ → F ∖ supp 0 ˙⁡ P ⊆ B
71 70 sselda ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → e ∈ B
72 1 2 3 67 71 ringlzd ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → 0 ˙ · ˙ e = 0 ˙
73 66 72 eqtrd ⊢ φ ∧ e ∈ F ∖ supp 0 ˙⁡ P → P ⁡ e · ˙ e = 0 ˙
74 57 adantr ⊢ φ ∧ e ∈ F → R ∈ Ring
75 1 subrgss ⊢ E ∈ SubRing ⁡ R → E ⊆ B
76 6 75 syl ⊢ φ → E ⊆ B
77 8 76 fssd ⊢ φ → P : F ⟶ B
78 77 ffvelcdmda ⊢ φ ∧ e ∈ F → P ⁡ e ∈ B
79 69 sselda ⊢ φ ∧ e ∈ F → e ∈ B
80 1 2 74 78 79 ringcld ⊢ φ ∧ e ∈ F → P ⁡ e · ˙ e ∈ B
81 1 3 58 7 73 49 80 26 gsummptres2 ⊢ φ → ∑ R e ∈ F P ⁡ e · ˙ e = ∑ R e ∈ P supp 0 ˙ P ⁡ e · ˙ e
82 nfcv ⊢ Ⅎ _ e P ⁡ w ⁡ 1 · ˙ w ⁡ 1
83 fveq2 ⊢ e = w ⁡ 1 → P ⁡ e = P ⁡ w ⁡ 1
84 id ⊢ e = w ⁡ 1 → e = w ⁡ 1
85 83 84 oveq12d ⊢ e = w ⁡ 1 → P ⁡ e · ˙ e = P ⁡ w ⁡ 1 · ˙ w ⁡ 1
86 ssidd ⊢ φ → B ⊆ B
87 26 sselda ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → e ∈ F
88 87 80 syldan ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → P ⁡ e · ˙ e ∈ B
89 fveq1 ⊢ w = ⟨“ P ⁡ f f ”⟩ → w ⁡ 1 = ⟨“ P ⁡ f f ”⟩ ⁡ 1
90 89 adantl ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w ⁡ 1 = ⟨“ P ⁡ f f ”⟩ ⁡ 1
91 s2fv1 ⊢ f ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ f f ”⟩ ⁡ 1 = f
92 91 ad2antlr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ⟨“ P ⁡ f f ”⟩ ⁡ 1 = f
93 90 92 eqtrd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w ⁡ 1 = f
94 simplr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f ∈ supp 0 ˙⁡ P
95 93 94 eqeltrd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w ⁡ 1 ∈ supp 0 ˙⁡ P
96 11 eleq2i ⊢ w ∈ T ↔ w ∈ ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
97 96 bilani ⊢ φ ∧ w ∈ T → w ∈ ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
98 35 97 elrnmpt2d ⊢ φ ∧ w ∈ T → ∃ f ∈ supp 0 ˙⁡ P w = ⟨“ P ⁡ f f ”⟩
99 95 98 r19.29a ⊢ φ ∧ w ∈ T → w ⁡ 1 ∈ supp 0 ˙⁡ P
100 fveq2 ⊢ f = e → P ⁡ f = P ⁡ e
101 id ⊢ f = e → f = e
102 100 101 s2eqd ⊢ f = e → ⟨“ P ⁡ f f ”⟩ = ⟨“ P ⁡ e e ”⟩
103 102 cbvmptv ⊢ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ = e ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ e e ”⟩
104 simpr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → e ∈ supp 0 ˙⁡ P
105 77 adantr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → P : F ⟶ B
106 105 87 ffvelcdmd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → P ⁡ e ∈ B
107 26 69 sstrd ⊢ φ → P supp 0 ˙ ⊆ B
108 107 sselda ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → e ∈ B
109 106 108 s2cld ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ∈ Word B
110 103 104 109 elrnmpt1d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ∈ ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
111 110 11 eleqtrrdi ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ∈ T
112 simpr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w = ⟨“ P ⁡ f f ”⟩
113 84 ad3antlr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → e = w ⁡ 1
114 112 fveq1d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w ⁡ 1 = ⟨“ P ⁡ f f ”⟩ ⁡ 1
115 91 ad2antlr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ⟨“ P ⁡ f f ”⟩ ⁡ 1 = f
116 113 114 115 3eqtrrd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f = e
117 116 fveq2d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ f = P ⁡ e
118 117 116 s2eqd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ⟨“ P ⁡ f f ”⟩ = ⟨“ P ⁡ e e ”⟩
119 112 118 eqtrd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w = ⟨“ P ⁡ e e ”⟩
120 98 ad4ant13 ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 → ∃ f ∈ supp 0 ˙⁡ P w = ⟨“ P ⁡ f f ”⟩
121 119 120 r19.29a ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 → w = ⟨“ P ⁡ e e ”⟩
122 simpr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → w = ⟨“ P ⁡ e e ”⟩
123 122 fveq1d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → w ⁡ 1 = ⟨“ P ⁡ e e ”⟩ ⁡ 1
124 s2fv1 ⊢ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ⁡ 1 = e
125 124 ad3antlr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → ⟨“ P ⁡ e e ”⟩ ⁡ 1 = e
126 123 125 eqtr2d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → e = w ⁡ 1
127 121 126 impbida ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T → e = w ⁡ 1 ↔ w = ⟨“ P ⁡ e e ”⟩
128 111 127 reu6dv ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ∃! w ∈ T e = w ⁡ 1
129 82 1 3 85 58 49 86 88 99 128 gsummptf1o ⊢ φ → ∑ R e ∈ P supp 0 ˙ P ⁡ e · ˙ e = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
130 81 129 eqtrd ⊢ φ → ∑ R e ∈ F P ⁡ e · ˙ e = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
131 22 adantr ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → Word E ∪ F ∈ V
132 38 adantr ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → T ⊆ Word E ∪ F
133 simpr ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → w ∈ Word E ∪ F ∖ T
134 ind0 ⊢ Word E ∪ F ∈ V ∧ T ⊆ Word E ∪ F ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 0
135 131 132 133 134 syl3anc ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 0
136 135 oveq1d ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = 0 ⋅ R ∑ mulGrp R w
137 eqid ⊢ mulGrp R = mulGrp R
138 137 crngmgp ⊢ R ∈ CRing → mulGrp R ∈ CMnd
139 5 138 syl ⊢ φ → mulGrp R ∈ CMnd
140 139 cmnmndd ⊢ φ → mulGrp R ∈ Mnd
141 76 69 unssd ⊢ φ → E ∪ F ⊆ B
142 sswrd ⊢ E ∪ F ⊆ B → Word E ∪ F ⊆ Word B
143 141 142 syl ⊢ φ → Word E ∪ F ⊆ Word B
144 143 ssdifssd ⊢ φ → Word E ∪ F ∖ T ⊆ Word B
145 144 sselda ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → w ∈ Word B
146 137 1 mgpbas ⊢ B = Base mulGrp R
147 146 gsumwcl ⊢ mulGrp R ∈ Mnd ∧ w ∈ Word B → ∑ mulGrp R w ∈ B
148 140 145 147 syl2an2r ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → ∑ mulGrp R w ∈ B
149 eqid ⊢ ⋅ R = ⋅ R
150 1 3 149 mulg0 ⊢ ∑ mulGrp R w ∈ B → 0 ⋅ R ∑ mulGrp R w = 0 ˙
151 148 150 syl ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 0 ⋅ R ∑ mulGrp R w = 0 ˙
152 136 151 eqtrd ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = 0 ˙
153 5 crnggrpd ⊢ φ → R ∈ Grp
154 153 adantr ⊢ φ ∧ w ∈ Word E ∪ F → R ∈ Grp
155 44 ffvelcdmda ⊢ φ ∧ w ∈ Word E ∪ F → 𝟙 Word E ∪ F ⁡ T ⁡ w ∈ ℤ
156 143 sselda ⊢ φ ∧ w ∈ Word E ∪ F → w ∈ Word B
157 140 156 147 syl2an2r ⊢ φ ∧ w ∈ Word E ∪ F → ∑ mulGrp R w ∈ B
158 1 149 154 155 157 mulgcld ⊢ φ ∧ w ∈ Word E ∪ F → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w ∈ B
159 1 3 58 22 152 53 158 38 gsummptres2 ⊢ φ → ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = ∑ R w ∈ T 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
160 38 143 sstrd ⊢ φ → T ⊆ Word B
161 160 sselda ⊢ φ ∧ w ∈ T → w ∈ Word B
162 140 161 147 syl2an2r ⊢ φ ∧ w ∈ T → ∑ mulGrp R w ∈ B
163 1 149 mulg1 ⊢ ∑ mulGrp R w ∈ B → 1 ⋅ R ∑ mulGrp R w = ∑ mulGrp R w
164 162 163 syl ⊢ φ ∧ w ∈ T → 1 ⋅ R ∑ mulGrp R w = ∑ mulGrp R w
165 22 adantr ⊢ φ ∧ w ∈ T → Word E ∪ F ∈ V
166 38 adantr ⊢ φ ∧ w ∈ T → T ⊆ Word E ∪ F
167 simpr ⊢ φ ∧ w ∈ T → w ∈ T
168 ind1 ⊢ Word E ∪ F ∈ V ∧ T ⊆ Word E ∪ F ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 1
169 165 166 167 168 syl3anc ⊢ φ ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 1
170 169 oveq1d ⊢ φ ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = 1 ⋅ R ∑ mulGrp R w
171 140 ad3antrrr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → mulGrp R ∈ Mnd
172 77 ad3antrrr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P : F ⟶ B
173 27 ad4ant13 ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f ∈ F
174 172 173 ffvelcdmd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ f ∈ B
175 107 ad3antrrr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P supp 0 ˙ ⊆ B
176 175 94 sseldd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f ∈ B
177 137 2 mgpplusg ⊢ · ˙ = + mulGrp R
178 146 177 gsumws2 ⊢ mulGrp R ∈ Mnd ∧ P ⁡ f ∈ B ∧ f ∈ B → ∑ mulGrp R ⟨“ P ⁡ f f ”⟩ = P ⁡ f · ˙ f
179 171 174 176 178 syl3anc ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ∑ mulGrp R ⟨“ P ⁡ f f ”⟩ = P ⁡ f · ˙ f
180 simpr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w = ⟨“ P ⁡ f f ”⟩
181 180 oveq2d ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ∑ mulGrp R w = ∑ mulGrp R ⟨“ P ⁡ f f ”⟩
182 93 fveq2d ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ w ⁡ 1 = P ⁡ f
183 182 93 oveq12d ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ w ⁡ 1 · ˙ w ⁡ 1 = P ⁡ f · ˙ f
184 179 181 183 3eqtr4rd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ w ⁡ 1 · ˙ w ⁡ 1 = ∑ mulGrp R w
185 184 98 r19.29a ⊢ φ ∧ w ∈ T → P ⁡ w ⁡ 1 · ˙ w ⁡ 1 = ∑ mulGrp R w
186 164 170 185 3eqtr4d ⊢ φ ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = P ⁡ w ⁡ 1 · ˙ w ⁡ 1
187 186 mpteq2dva ⊢ φ → w ∈ T ⟼ 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = w ∈ T ⟼ P ⁡ w ⁡ 1 · ˙ w ⁡ 1
188 187 oveq2d ⊢ φ → ∑ R w ∈ T 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
189 159 188 eqtrd ⊢ φ → ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
190 130 10 189 3eqtr4d ⊢ φ → X = ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
191 16 56 190 rspcedvdw ⊢ φ → ∃ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
192 breq1 ⊢ h = i → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ i
193 192 cbvrabv ⊢ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h = i ∈ ℤ Word E ∪ F | finSupp 0 ⁡ i
194 1 137 149 4 193 57 141 elrgspn ⊢ φ → X ∈ N ⁡ E ∪ F ↔ ∃ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
195 191 194 mpbird ⊢ φ → X ∈ N ⁡ E ∪ F