Theorem elrgspnsubrunlem1 33907

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

Hypotheses

Ref	Expression
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

Ref	Expression
elrgspnsubrunlem1	⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)))

Distinct variable groups:   0 ,𝑒,𝑓   · ,𝑒,𝑓   𝐵,𝑒   𝑒,𝐸,𝑓   𝑒,𝐹,𝑓   𝑃,𝑒,𝑓   𝑅,𝑒,𝑓   𝑇,𝑒,𝑓   𝜑,𝑒,𝑓

Allowed substitution hints:   𝐵(𝑓)   𝑁(𝑒, 𝑓)   𝑋(𝑒, 𝑓)

Proof of Theorem elrgspnsubrunlem1

Dummy variables 𝑤 𝑔 𝑖 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq1 6915	. . . . . . 7 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑔‘𝑤) = (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤))
2	1	oveq1d 7466	. . . . . 6 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
3	2	mpteq2dv 5205	. . . . 5 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))
4	3	oveq2d 7467	. . . 4 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
5	4	eqeq2d 2774	. . 3 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) ↔ 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
6		breq1 5111	. . . 4 ⊢ (ℎ = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (ℎ finSupp 0 ↔ ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0))
7		zex 12742	. . . . . 6 ⊢ ℤ ∈ V
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → ℤ ∈ V)
9		elrgspnsubrun.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))
10		elrgspnsubrun.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))
11	9, 10	unexd 7800	. . . . . 6 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ V)
12		wrdexg 14710	. . . . . 6 ⊢ ((𝐸 ∪ 𝐹) ∈ V → Word (𝐸 ∪ 𝐹) ∈ V)
13	11, 12	syl 18	. . . . 5 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ∈ V)
14		elrgspnsubrunlem1.t	. . . . . . . 8 ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
15		ssun1 4179	. . . . . . . . . . . 12 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
16		elrgspnsubrunlem1.p1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:𝐹⟶𝐸)
17	16	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐸)
18		suppssdm 8232	. . . . . . . . . . . . . . 15 ⊢ (𝑃 supp 0 ) ⊆ dom 𝑃
19	18, 16	fssdm 6759	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐹)
20	19	sselda 3913	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ 𝐹)
21	17, 20	ffvelcdmd 7117	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ 𝐸)
22	15, 21	sselid 3911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ (𝐸 ∪ 𝐹))
23		ssun2 4180	. . . . . . . . . . . . 13 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
24	19, 23	sstrdi 3925	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ (𝐸 ∪ 𝐹))
25	24	sselda 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ (𝐸 ∪ 𝐹))
26	22, 25	s2cld 15064	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
27	26	ralrimiva 3158	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
28		eqid 2763	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
29	28	rnmptss 7155	. . . . . . . . 9 ⊢ (∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹) → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
30	27, 29	syl 18	. . . . . . . 8 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
31	14, 30	eqsstrid 3951	. . . . . . 7 ⊢ (𝜑 → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
32		indf 12366	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
33	13, 31, 32	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
34		0zd 12745	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
35		1zzd 12767	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
36	34, 35	prssd 4783	. . . . . 6 ⊢ (𝜑 → {0, 1} ⊆ ℤ)
37	33, 36	fssd 6757	. . . . 5 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶ℤ)
38	8, 13, 37	elmapdd 8899	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)))
39	33	ffund 6744	. . . . 5 ⊢ (𝜑 → Fun ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇))
40		indsupp 33530	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
41	13, 31, 40	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
42		elrgspnsubrunlem1.p2	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp 0 )
43	42	fsuppimpd 9399	. . . . . . . 8 ⊢ (𝜑 → (𝑃 supp 0 ) ∈ Fin)
44		mptfi 9378	. . . . . . . 8 ⊢ ((𝑃 supp 0 ) ∈ Fin → (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
45		rnfi 9367	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
46	43, 44, 45	3syl 19	. . . . . . 7 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
47	14, 46	eqeltrid 2868	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ Fin)
48	41, 47	eqeltrd 2864	. . . . 5 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) ∈ Fin)
49	38, 34, 39, 48	isfsuppd 9396	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0)
50	6, 38, 49	elrabd 3650	. . 3 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0})
51		elrgspnsubrun.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
52		elrgspnsubrun.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
53		elrgspnsubrun.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CRing)
54	53	crngringd 20524	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
55	54	ringcmnd 20564	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
56	16	ffnd 6740	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 Fn 𝐹)
57	56	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑃 Fn 𝐹)
58	10	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝐹 ∈ (SubRing‘𝑅))
59	52	fvexi 6930	. . . . . . . . . 10 ⊢ 0 ∈ V
60	59	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 0 ∈ V)
61		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 )))
62	57, 58, 60, 61	fvdifsupp 8226	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → (𝑃‘𝑒) = 0 )
63	62	oveq1d 7466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = ( 0 · 𝑒))
64		elrgspnsubrun.t	. . . . . . . 8 ⊢ · = (.r‘𝑅)
65	54	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑅 ∈ Ring)
66	51	subrgss 20875	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubRing‘𝑅) → 𝐹 ⊆ 𝐵)
67	10, 66	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
68	67	ssdifssd 4086	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∖ (𝑃 supp 0 )) ⊆ 𝐵)
69	68	sselda 3913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ 𝐵)
70	51, 64, 52, 65, 69	ringlzd 20577	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ( 0 · 𝑒) = 0 )
71	63, 70	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = 0 )
72	54	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑅 ∈ Ring)
73	51	subrgss 20875	. . . . . . . . . 10 ⊢ (𝐸 ∈ (SubRing‘𝑅) → 𝐸 ⊆ 𝐵)
74	9, 73	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝐵)
75	16, 74	fssd 6757	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐹⟶𝐵)
76	75	ffvelcdmda 7116	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → (𝑃‘𝑒) ∈ 𝐵)
77	67	sselda 3913	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒 ∈ 𝐵)
78	51, 64, 72, 76, 77	ringcld 20535	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
79	51, 52, 55, 10, 71, 43, 78, 19	gsummptres2 33713	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))))
80		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑒((𝑃‘(𝑤‘1)) · (𝑤‘1))
81		fveq2 6916	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → (𝑃‘𝑒) = (𝑃‘(𝑤‘1)))
82		id 23	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → 𝑒 = (𝑤‘1))
83	81, 82	oveq12d 7469	. . . . . 6 ⊢ (𝑒 = (𝑤‘1) → ((𝑃‘𝑒) · 𝑒) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
84		ssidd 3936	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
85	19	sselda 3913	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐹)
86	85, 78	syldan 603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
87		fveq1 6915	. . . . . . . . . 10 ⊢ (𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩ → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
88	87	adantl 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
89		s2fv1 15081	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
90	89	ad2antlr 740	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
91	88, 90	eqtrd 2798	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = 𝑓)
92		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ (𝑃 supp 0 ))
93	91, 92	eqeltrd 2864	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) ∈ (𝑃 supp 0 ))
94	14	eleq2i 2856	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
95	94	bilani 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
96	28, 95	elrnmpt2d 5960	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
97	93, 96	r19.29a 3174	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝑤‘1) ∈ (𝑃 supp 0 ))
98		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → (𝑃‘𝑓) = (𝑃‘𝑒))
99		id 23	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → 𝑓 = 𝑒)
100	98, 99	s2eqd 15056	. . . . . . . . . 10 ⊢ (𝑓 = 𝑒 → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
101	100	cbvmptv 5215	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑒 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑒)𝑒”⟩)
102		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ (𝑃 supp 0 ))
103	75	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐵)
104	103, 85	ffvelcdmd 7117	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → (𝑃‘𝑒) ∈ 𝐵)
105	19, 67	sstrd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐵)
106	105	sselda 3913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐵)
107	104, 106	s2cld 15064	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ Word 𝐵)
108	101, 102, 107	elrnmpt1d 5958	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
109	108, 14	eleqtrrdi 2875	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ 𝑇)
110		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
111	82	ad3antlr 744	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑒 = (𝑤‘1))
112	110	fveq1d 6918	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
113	89	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
114	111, 112, 113	3eqtrrd 2803	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 = 𝑒)
115	114	fveq2d 6920	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) = (𝑃‘𝑒))
116	115, 114	s2eqd 15056	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
117	110, 116	eqtrd 2798	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
118	96	ad4ant13 764	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
119	117, 118	r19.29a 3174	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
120		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
121	120	fveq1d 6918	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑒)𝑒”⟩‘1))
122		s2fv1 15081	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
123	122	ad3antlr 744	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
124	121, 123	eqtr2d 2799	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑒 = (𝑤‘1))
125	119, 124	impbida 813	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) → (𝑒 = (𝑤‘1) ↔ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩))
126	109, 125	reu6dv 33168	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ∃!𝑤 ∈ 𝑇 𝑒 = (𝑤‘1))
127	80, 51, 52, 83, 55, 43, 84, 86, 97, 126	gsummptf1o 20228	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
128	79, 127	eqtrd 2798	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
129		elrgspnsubrunlem1.x	. . . 4 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))))
130	13	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → Word (𝐸 ∪ 𝐹) ∈ V)
131	31	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
132		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇))
133		ind0 12370	. . . . . . . . 9 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
134	130, 131, 132, 133	syl3anc 1399	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
135	134	oveq1d 7466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
136		eqid 2763	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
137	136	crngmgp 20518	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
138	53, 137	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
139	138	cmnmndd 20069	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
140	74, 67	unssd 4193	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ 𝐵)
141		sswrd 14708	. . . . . . . . . . . 12 ⊢ ((𝐸 ∪ 𝐹) ⊆ 𝐵 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
142	140, 141	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
143	142	ssdifssd 4086	. . . . . . . . . 10 ⊢ (𝜑 → (Word (𝐸 ∪ 𝐹) ∖ 𝑇) ⊆ Word 𝐵)
144	143	sselda 3913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ Word 𝐵)
145	136, 51	mgpbas 20416	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
146	145	gsumwcl 19085	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
147	139, 144, 146	syl2an2r 698	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
148		eqid 2763	. . . . . . . . 9 ⊢ (.g‘𝑅) = (.g‘𝑅)
149	51, 52, 148	mulg0 19334	. . . . . . . 8 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
150	147, 149	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
151	135, 150	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
152	53	crnggrpd 20525	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
153	152	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑅 ∈ Grp)
154	37	ffvelcdmda 7116	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) ∈ ℤ)
155	142	sselda 3913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word 𝐵)
156	139, 155, 146	syl2an2r 698	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
157	51, 148, 153, 154, 156	mulgcld 19356	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) ∈ 𝐵)
158	51, 52, 55, 13, 151, 47, 157, 31	gsummptres2 33713	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
159	31, 142	sstrd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ Word 𝐵)
160	159	sselda 3913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ Word 𝐵)
161	139, 160, 146	syl2an2r 698	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
162	51, 148	mulg1 19341	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((mulGrp‘𝑅) Σg 𝑤))
163	161, 162	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((mulGrp‘𝑅) Σg 𝑤))
164	13	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → Word (𝐸 ∪ 𝐹) ∈ V)
165	31	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
166		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ 𝑇)
167		ind1 12369	. . . . . . . . . 10 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
168	164, 165, 166, 167	syl3anc 1399	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
169	168	oveq1d 7466	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
170	139	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (mulGrp‘𝑅) ∈ Mnd)
171	75	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑃:𝐹⟶𝐵)
172	20	ad4ant13 764	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐹)
173	171, 172	ffvelcdmd 7117	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) ∈ 𝐵)
174	105	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃 supp 0 ) ⊆ 𝐵)
175	174, 92	sseldd 3914	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐵)
176	136, 64	mgpplusg 20415	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
177	145, 176	gsumws2 19088	. . . . . . . . . . 11 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ (𝑃‘𝑓) ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
178	170, 173, 175, 177	syl3anc 1399	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
179		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
180	179	oveq2d 7467	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg 𝑤) = ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩))
181	91	fveq2d 6920	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘(𝑤‘1)) = (𝑃‘𝑓))
182	181, 91	oveq12d 7469	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((𝑃‘𝑓) · 𝑓))
183	178, 180, 182	3eqtr4rd 2809	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
184	183, 96	r19.29a 3174	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
185	163, 169, 184	3eqtr4d 2808	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
186	185	mpteq2dva 5204	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1))))
187	186	oveq2d 7467	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
188	158, 187	eqtrd 2798	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
189	128, 129, 188	3eqtr4d 2808	. . 3 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
190	5, 50, 189	rspcedvdw 3583	. 2 ⊢ (𝜑 → ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
191		elrgspnsubrun.n	. . 3 ⊢ 𝑁 = (RingSpan‘𝑅)
192		breq1 5111	. . . 4 ⊢ (ℎ = 𝑖 → (ℎ finSupp 0 ↔ 𝑖 finSupp 0))
193	192	cbvrabv 3426	. . 3 ⊢ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0} = {𝑖 ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ 𝑖 finSupp 0}
194	51, 136, 148, 191, 193, 54, 140	elrgspn 33906	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)) ↔ ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
195	190, 194	mpbird 260	1 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∪ cun 4152  {cpr 4590   class class class wbr 5108   ↦ cmpt 5192  ran crn 5659   Fn wfn 6561  ⟶wf 6562  ‘cfv 6566  (class class class)co 7451   supp csupp 8214   ↑_m cmap 8885  Fincfn 9011   finSupp cfsupp 9391  0cc0 11239  1c1 11240  𝟭cind 12360  ℤcz 12733  Word cword 14699  ⟨“cs2 15034  Basecbs 17431  ._rcmulr 17473  0_gc0g 17660   Σ_g cgsu 17661  Mndcmnd 18973  Grpcgrp 19194  ._gcmg 19327  CMndccmn 20045  mulGrpcmgp 20411  Ringcrg 20510  CRingccrg 20511  SubRingcsubrg 20872  RingSpancrgspn 20913

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317  ax-addf 11318

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-of 7725  df-om 7912  df-1st 8035  df-2nd 8036  df-supp 8215  df-tpos 8281  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-2o 8515  df-er 8755  df-map 8887  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-fsupp 9392  df-sup 9471  df-oi 9541  df-card 10057  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-ind 12361  df-nn 12376  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452  df-n0 12647  df-z 12734  df-dec 12855  df-uz 13006  df-rp 13161  df-fz 13680  df-fzo 13829  df-seq 14185  df-exp 14245  df-hash 14516  df-word 14700  df-concat 14757  df-s1 14784  df-substr 14831  df-pfx 14863  df-s2 15041  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-clim 15699  df-sum 15898  df-struct 17369  df-sets 17386  df-slot 17404  df-ndx 17416  df-base 17432  df-ress 17453  df-plusg 17486  df-mulr 17487  df-starv 17488  df-tset 17492  df-ple 17493  df-ds 17495  df-unif 17496  df-euf 17499  df-0g 17662  df-gsum 17663  df-mre 17806  df-mrc 17807  df-acs 17809  df-mgm 18866  df-sgrp 18958  df-mnd 18974  df-mhm 19028  df-submnd 19029  df-grp 19197  df-minusg 19198  df-mulg 19328  df-subg 19383  df-ghm 19478  df-cntz 19582  df-cmn 20047  df-abl 20048  df-mgp 20412  df-rng 20426  df-ur 20459  df-ring 20512  df-cring 20513  df-oppr 20618  df-subrng 20849  df-subrg 20873  df-rgspn 20914  df-cnfld 21730  df-zring 21807

This theorem is used by:  elrgspnsubrun  33909