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