Metamath Proof Explorer

Theorem elrgspnsubrunlem1

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

Ref Expression
Hypotheses elrgspnsubrun.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
elrgspnsubrun.t ⊢ · = ( .r ‘ 𝑅 )
elrgspnsubrun.z ⊢ 0 = ( 0g ‘ 𝑅 )
elrgspnsubrun.n ⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
elrgspnsubrun.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
elrgspnsubrun.e ⊢ ( 𝜑 → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
elrgspnsubrun.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
elrgspnsubrunlem1.p1 ⊢ ( 𝜑 → 𝑃 : 𝐹 ⟶ 𝐸 )
elrgspnsubrunlem1.p2 ⊢ ( 𝜑 → 𝑃 finSupp 0 )
elrgspnsubrunlem1.x ⊢ ( 𝜑 → 𝑋 = ( 𝑅 Σg ( 𝑒 ∈ 𝐹 ↦ ( ( 𝑃 ‘ 𝑒 ) · 𝑒 ) ) ) )
elrgspnsubrunlem1.t ⊢ 𝑇 = ran ( 𝑓 ∈ ( 𝑃 supp 0 ) ↦ ⟨“ ( 𝑃 ‘ 𝑓 ) 𝑓 ”⟩ )
Assertion elrgspnsubrunlem1 ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ ( 𝐸 ∪ 𝐹 ) ) )

Proof

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