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 biimpi ⊢ w ∈ T → w ∈ ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
98 97 adantl ⊢ φ ∧ w ∈ T → w ∈ ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
99 35 98 elrnmpt2d ⊢ φ ∧ w ∈ T → ∃ f ∈ supp 0 ˙⁡ P w = ⟨“ P ⁡ f f ”⟩
100 95 99 r19.29a ⊢ φ ∧ w ∈ T → w ⁡ 1 ∈ supp 0 ˙⁡ P
101 fveq2 ⊢ f = e → P ⁡ f = P ⁡ e
102 id ⊢ f = e → f = e
103 101 102 s2eqd ⊢ f = e → ⟨“ P ⁡ f f ”⟩ = ⟨“ P ⁡ e e ”⟩
104 103 cbvmptv ⊢ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩ = e ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ e e ”⟩
105 simpr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → e ∈ supp 0 ˙⁡ P
106 77 adantr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → P : F ⟶ B
107 106 87 ffvelcdmd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → P ⁡ e ∈ B
108 26 69 sstrd ⊢ φ → P supp 0 ˙ ⊆ B
109 108 sselda ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → e ∈ B
110 107 109 s2cld ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ∈ Word B
111 104 105 110 elrnmpt1d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ∈ ran ⁡ f ∈ supp 0 ˙⁡ P ⟼ ⟨“ P ⁡ f f ”⟩
112 111 11 eleqtrrdi ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ∈ T
113 simpr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w = ⟨“ P ⁡ f f ”⟩
114 84 ad3antlr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → e = w ⁡ 1
115 113 fveq1d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w ⁡ 1 = ⟨“ P ⁡ f f ”⟩ ⁡ 1
116 91 ad2antlr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ⟨“ P ⁡ f f ”⟩ ⁡ 1 = f
117 114 115 116 3eqtrrd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f = e
118 117 fveq2d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ f = P ⁡ e
119 118 117 s2eqd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ⟨“ P ⁡ f f ”⟩ = ⟨“ P ⁡ e e ”⟩
120 113 119 eqtrd ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w = ⟨“ P ⁡ e e ”⟩
121 99 ad4ant13 ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 → ∃ f ∈ supp 0 ˙⁡ P w = ⟨“ P ⁡ f f ”⟩
122 120 121 r19.29a ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ e = w ⁡ 1 → w = ⟨“ P ⁡ e e ”⟩
123 simpr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → w = ⟨“ P ⁡ e e ”⟩
124 123 fveq1d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → w ⁡ 1 = ⟨“ P ⁡ e e ”⟩ ⁡ 1
125 s2fv1 ⊢ e ∈ supp 0 ˙⁡ P → ⟨“ P ⁡ e e ”⟩ ⁡ 1 = e
126 125 ad3antlr ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → ⟨“ P ⁡ e e ”⟩ ⁡ 1 = e
127 124 126 eqtr2d ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T ∧ w = ⟨“ P ⁡ e e ”⟩ → e = w ⁡ 1
128 122 127 impbida ⊢ φ ∧ e ∈ supp 0 ˙⁡ P ∧ w ∈ T → e = w ⁡ 1 ↔ w = ⟨“ P ⁡ e e ”⟩
129 112 128 reu6dv ⊢ φ ∧ e ∈ supp 0 ˙⁡ P → ∃! w ∈ T e = w ⁡ 1
130 82 1 3 85 58 49 86 88 100 129 gsummptf1o ⊢ φ → ∑ R e ∈ P supp 0 ˙ P ⁡ e · ˙ e = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
131 81 130 eqtrd ⊢ φ → ∑ R e ∈ F P ⁡ e · ˙ e = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
132 22 adantr ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → Word E ∪ F ∈ V
133 38 adantr ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → T ⊆ Word E ∪ F
134 simpr ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → w ∈ Word E ∪ F ∖ T
135 ind0 ⊢ Word E ∪ F ∈ V ∧ T ⊆ Word E ∪ F ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 0
136 132 133 134 135 syl3anc ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 0
137 136 oveq1d ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = 0 ⋅ R ∑ mulGrp R w
138 eqid ⊢ mulGrp R = mulGrp R
139 138 crngmgp ⊢ R ∈ CRing → mulGrp R ∈ CMnd
140 5 139 syl ⊢ φ → mulGrp R ∈ CMnd
141 140 cmnmndd ⊢ φ → mulGrp R ∈ Mnd
142 76 69 unssd ⊢ φ → E ∪ F ⊆ B
143 sswrd ⊢ E ∪ F ⊆ B → Word E ∪ F ⊆ Word B
144 142 143 syl ⊢ φ → Word E ∪ F ⊆ Word B
145 144 ssdifssd ⊢ φ → Word E ∪ F ∖ T ⊆ Word B
146 145 sselda ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → w ∈ Word B
147 138 1 mgpbas ⊢ B = Base mulGrp R
148 147 gsumwcl ⊢ mulGrp R ∈ Mnd ∧ w ∈ Word B → ∑ mulGrp R w ∈ B
149 141 146 148 syl2an2r ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → ∑ mulGrp R w ∈ B
150 eqid ⊢ ⋅ R = ⋅ R
151 1 3 150 mulg0 ⊢ ∑ mulGrp R w ∈ B → 0 ⋅ R ∑ mulGrp R w = 0 ˙
152 149 151 syl ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 0 ⋅ R ∑ mulGrp R w = 0 ˙
153 137 152 eqtrd ⊢ φ ∧ w ∈ Word E ∪ F ∖ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = 0 ˙
154 5 crnggrpd ⊢ φ → R ∈ Grp
155 154 adantr ⊢ φ ∧ w ∈ Word E ∪ F → R ∈ Grp
156 44 ffvelcdmda ⊢ φ ∧ w ∈ Word E ∪ F → 𝟙 Word E ∪ F ⁡ T ⁡ w ∈ ℤ
157 144 sselda ⊢ φ ∧ w ∈ Word E ∪ F → w ∈ Word B
158 141 157 148 syl2an2r ⊢ φ ∧ w ∈ Word E ∪ F → ∑ mulGrp R w ∈ B
159 1 150 155 156 158 mulgcld ⊢ φ ∧ w ∈ Word E ∪ F → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w ∈ B
160 1 3 58 22 153 53 159 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
161 38 144 sstrd ⊢ φ → T ⊆ Word B
162 161 sselda ⊢ φ ∧ w ∈ T → w ∈ Word B
163 141 162 148 syl2an2r ⊢ φ ∧ w ∈ T → ∑ mulGrp R w ∈ B
164 1 150 mulg1 ⊢ ∑ mulGrp R w ∈ B → 1 ⋅ R ∑ mulGrp R w = ∑ mulGrp R w
165 163 164 syl ⊢ φ ∧ w ∈ T → 1 ⋅ R ∑ mulGrp R w = ∑ mulGrp R w
166 22 adantr ⊢ φ ∧ w ∈ T → Word E ∪ F ∈ V
167 38 adantr ⊢ φ ∧ w ∈ T → T ⊆ Word E ∪ F
168 simpr ⊢ φ ∧ w ∈ T → w ∈ T
169 ind1 ⊢ Word E ∪ F ∈ V ∧ T ⊆ Word E ∪ F ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 1
170 166 167 168 169 syl3anc ⊢ φ ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w = 1
171 170 oveq1d ⊢ φ ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = 1 ⋅ R ∑ mulGrp R w
172 141 ad3antrrr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → mulGrp R ∈ Mnd
173 77 ad3antrrr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P : F ⟶ B
174 27 ad4ant13 ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f ∈ F
175 173 174 ffvelcdmd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ f ∈ B
176 108 ad3antrrr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P supp 0 ˙ ⊆ B
177 176 94 sseldd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → f ∈ B
178 138 2 mgpplusg ⊢ · ˙ = + mulGrp R
179 147 178 gsumws2 ⊢ mulGrp R ∈ Mnd ∧ P ⁡ f ∈ B ∧ f ∈ B → ∑ mulGrp R ⟨“ P ⁡ f f ”⟩ = P ⁡ f · ˙ f
180 172 175 177 179 syl3anc ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ∑ mulGrp R ⟨“ P ⁡ f f ”⟩ = P ⁡ f · ˙ f
181 simpr ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → w = ⟨“ P ⁡ f f ”⟩
182 181 oveq2d ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → ∑ mulGrp R w = ∑ mulGrp R ⟨“ P ⁡ f f ”⟩
183 93 fveq2d ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ w ⁡ 1 = P ⁡ f
184 183 93 oveq12d ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ w ⁡ 1 · ˙ w ⁡ 1 = P ⁡ f · ˙ f
185 180 182 184 3eqtr4rd ⊢ φ ∧ w ∈ T ∧ f ∈ supp 0 ˙⁡ P ∧ w = ⟨“ P ⁡ f f ”⟩ → P ⁡ w ⁡ 1 · ˙ w ⁡ 1 = ∑ mulGrp R w
186 185 99 r19.29a ⊢ φ ∧ w ∈ T → P ⁡ w ⁡ 1 · ˙ w ⁡ 1 = ∑ mulGrp R w
187 165 171 186 3eqtr4d ⊢ φ ∧ w ∈ T → 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = P ⁡ w ⁡ 1 · ˙ w ⁡ 1
188 187 mpteq2dva ⊢ φ → w ∈ T ⟼ 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = w ∈ T ⟼ P ⁡ w ⁡ 1 · ˙ w ⁡ 1
189 188 oveq2d ⊢ φ → ∑ R w ∈ T 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
190 160 189 eqtrd ⊢ φ → ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w = ∑ R w ∈ T P ⁡ w ⁡ 1 · ˙ w ⁡ 1
191 131 10 190 3eqtr4d ⊢ φ → X = ∑ R w ∈ Word E ∪ F 𝟙 Word E ∪ F ⁡ T ⁡ w ⋅ R ∑ mulGrp R w
192 16 56 191 rspcedvdw ⊢ φ → ∃ g ∈ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h X = ∑ R w ∈ Word E ∪ F g ⁡ w ⋅ R ∑ mulGrp R w
193 breq1 ⊢ h = i → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ i
194 193 cbvrabv ⊢ h ∈ ℤ Word E ∪ F | finSupp 0 ⁡ h = i ∈ ℤ Word E ∪ F | finSupp 0 ⁡ i
195 1 138 150 4 194 57 142 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
196 192 195 mpbird ⊢ φ → X ∈ N ⁡ E ∪ F