Theorem elrgspnsubrunlem1 33205

Description: Lemma for elrgspnsubrun 33207, 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 6860	. . . . . . 7 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑔‘𝑤) = (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤))
2	1	oveq1d 7405	. . . . . 6 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
3	2	mpteq2dv 5204	. . . . 5 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))
4	3	oveq2d 7406	. . . 4 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
5	4	eqeq2d 2741	. . 3 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) ↔ 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
6		breq1 5113	. . . 4 ⊢ (ℎ = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (ℎ finSupp 0 ↔ ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0))
7		zex 12545	. . . . . 6 ⊢ ℤ ∈ V
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → ℤ ∈ V)
9		elrgspnsubrun.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))
10		elrgspnsubrun.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))
11	9, 10	unexd 7733	. . . . . 6 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ V)
12		wrdexg 14496	. . . . . 6 ⊢ ((𝐸 ∪ 𝐹) ∈ V → Word (𝐸 ∪ 𝐹) ∈ V)
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ∈ V)
14		elrgspnsubrunlem1.t	. . . . . . . 8 ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
15		ssun1 4144	. . . . . . . . . . . 12 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
16		elrgspnsubrunlem1.p1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:𝐹⟶𝐸)
17	16	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐸)
18		suppssdm 8159	. . . . . . . . . . . . . . 15 ⊢ (𝑃 supp 0 ) ⊆ dom 𝑃
19	18, 16	fssdm 6710	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐹)
20	19	sselda 3949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ 𝐹)
21	17, 20	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ 𝐸)
22	15, 21	sselid 3947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ (𝐸 ∪ 𝐹))
23		ssun2 4145	. . . . . . . . . . . . 13 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
24	19, 23	sstrdi 3962	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ (𝐸 ∪ 𝐹))
25	24	sselda 3949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ (𝐸 ∪ 𝐹))
26	22, 25	s2cld 14844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
27	26	ralrimiva 3126	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
28		eqid 2730	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
29	28	rnmptss 7098	. . . . . . . . 9 ⊢ (∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹) → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
30	27, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
31	14, 30	eqsstrid 3988	. . . . . . 7 ⊢ (𝜑 → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
32		indf 32785	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
33	13, 31, 32	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
34		0zd 12548	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
35		1zzd 12571	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
36	34, 35	prssd 4789	. . . . . 6 ⊢ (𝜑 → {0, 1} ⊆ ℤ)
37	33, 36	fssd 6708	. . . . 5 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶ℤ)
38	8, 13, 37	elmapdd 8817	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)))
39	33	ffund 6695	. . . . 5 ⊢ (𝜑 → Fun ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇))
40		indsupp 32797	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
41	13, 31, 40	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
42		elrgspnsubrunlem1.p2	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp 0 )
43	42	fsuppimpd 9327	. . . . . . . 8 ⊢ (𝜑 → (𝑃 supp 0 ) ∈ Fin)
44		mptfi 9309	. . . . . . . 8 ⊢ ((𝑃 supp 0 ) ∈ Fin → (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
45		rnfi 9298	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
46	43, 44, 45	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
47	14, 46	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ Fin)
48	41, 47	eqeltrd 2829	. . . . 5 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) ∈ Fin)
49	38, 34, 39, 48	isfsuppd 9324	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0)
50	6, 38, 49	elrabd 3664	. . 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 20162	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
55	54	ringcmnd 20200	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
56	16	ffnd 6692	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 Fn 𝐹)
57	56	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑃 Fn 𝐹)
58	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝐹 ∈ (SubRing‘𝑅))
59	52	fvexi 6875	. . . . . . . . . 10 ⊢ 0 ∈ V
60	59	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 0 ∈ V)
61		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 )))
62	57, 58, 60, 61	fvdifsupp 8153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → (𝑃‘𝑒) = 0 )
63	62	oveq1d 7405	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = ( 0 · 𝑒))
64		elrgspnsubrun.t	. . . . . . . 8 ⊢ · = (.r‘𝑅)
65	54	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑅 ∈ Ring)
66	51	subrgss 20488	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubRing‘𝑅) → 𝐹 ⊆ 𝐵)
67	10, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
68	67	ssdifssd 4113	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∖ (𝑃 supp 0 )) ⊆ 𝐵)
69	68	sselda 3949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ 𝐵)
70	51, 64, 52, 65, 69	ringlzd 20211	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ( 0 · 𝑒) = 0 )
71	63, 70	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = 0 )
72	54	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑅 ∈ Ring)
73	51	subrgss 20488	. . . . . . . . . 10 ⊢ (𝐸 ∈ (SubRing‘𝑅) → 𝐸 ⊆ 𝐵)
74	9, 73	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝐵)
75	16, 74	fssd 6708	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐹⟶𝐵)
76	75	ffvelcdmda 7059	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → (𝑃‘𝑒) ∈ 𝐵)
77	67	sselda 3949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒 ∈ 𝐵)
78	51, 64, 72, 76, 77	ringcld 20176	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
79	51, 52, 55, 10, 71, 43, 78, 19	gsummptres2 33000	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))))
80		nfcv 2892	. . . . . 6 ⊢ Ⅎ𝑒((𝑃‘(𝑤‘1)) · (𝑤‘1))
81		fveq2 6861	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → (𝑃‘𝑒) = (𝑃‘(𝑤‘1)))
82		id 22	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → 𝑒 = (𝑤‘1))
83	81, 82	oveq12d 7408	. . . . . 6 ⊢ (𝑒 = (𝑤‘1) → ((𝑃‘𝑒) · 𝑒) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
84		ssidd 3973	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
85	19	sselda 3949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐹)
86	85, 78	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
87		fveq1 6860	. . . . . . . . . 10 ⊢ (𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩ → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
88	87	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
89		s2fv1 14861	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
90	89	ad2antlr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
91	88, 90	eqtrd 2765	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = 𝑓)
92		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ (𝑃 supp 0 ))
93	91, 92	eqeltrd 2829	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) ∈ (𝑃 supp 0 ))
94	14	eleq2i 2821	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
95	94	biimpi 216	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
96	95	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
97	28, 96	elrnmpt2d 5933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
98	93, 97	r19.29a 3142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝑤‘1) ∈ (𝑃 supp 0 ))
99		fveq2 6861	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → (𝑃‘𝑓) = (𝑃‘𝑒))
100		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → 𝑓 = 𝑒)
101	99, 100	s2eqd 14836	. . . . . . . . . 10 ⊢ (𝑓 = 𝑒 → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
102	101	cbvmptv 5214	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑒 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑒)𝑒”⟩)
103		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ (𝑃 supp 0 ))
104	75	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐵)
105	104, 85	ffvelcdmd 7060	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → (𝑃‘𝑒) ∈ 𝐵)
106	19, 67	sstrd 3960	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐵)
107	106	sselda 3949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐵)
108	105, 107	s2cld 14844	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ Word 𝐵)
109	102, 103, 108	elrnmpt1d 5931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
110	109, 14	eleqtrrdi 2840	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ 𝑇)
111		simpr 484	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
112	82	ad3antlr 731	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑒 = (𝑤‘1))
113	111	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
114	89	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
115	112, 113, 114	3eqtrrd 2770	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 = 𝑒)
116	115	fveq2d 6865	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) = (𝑃‘𝑒))
117	116, 115	s2eqd 14836	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
118	111, 117	eqtrd 2765	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
119	97	ad4ant13 751	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
120	118, 119	r19.29a 3142	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
121		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
122	121	fveq1d 6863	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑒)𝑒”⟩‘1))
123		s2fv1 14861	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
124	123	ad3antlr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
125	122, 124	eqtr2d 2766	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑒 = (𝑤‘1))
126	120, 125	impbida 800	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) → (𝑒 = (𝑤‘1) ↔ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩))
127	110, 126	reu6dv 32409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ∃!𝑤 ∈ 𝑇 𝑒 = (𝑤‘1))
128	80, 51, 52, 83, 55, 43, 84, 86, 98, 127	gsummptf1o 19900	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
129	79, 128	eqtrd 2765	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
130		elrgspnsubrunlem1.x	. . . 4 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))))
131	13	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → Word (𝐸 ∪ 𝐹) ∈ V)
132	31	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
133		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇))
134		ind0 32788	. . . . . . . . 9 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
135	131, 132, 133, 134	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
136	135	oveq1d 7405	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
137		eqid 2730	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
138	137	crngmgp 20157	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
139	53, 138	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
140	139	cmnmndd 19741	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
141	74, 67	unssd 4158	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ 𝐵)
142		sswrd 14494	. . . . . . . . . . . 12 ⊢ ((𝐸 ∪ 𝐹) ⊆ 𝐵 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
143	141, 142	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
144	143	ssdifssd 4113	. . . . . . . . . 10 ⊢ (𝜑 → (Word (𝐸 ∪ 𝐹) ∖ 𝑇) ⊆ Word 𝐵)
145	144	sselda 3949	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ Word 𝐵)
146	137, 51	mgpbas 20061	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
147	146	gsumwcl 18773	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
148	140, 145, 147	syl2an2r 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
149		eqid 2730	. . . . . . . . 9 ⊢ (.g‘𝑅) = (.g‘𝑅)
150	51, 52, 149	mulg0 19013	. . . . . . . 8 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
151	148, 150	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
152	136, 151	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
153	53	crnggrpd 20163	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
154	153	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑅 ∈ Grp)
155	37	ffvelcdmda 7059	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) ∈ ℤ)
156	143	sselda 3949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word 𝐵)
157	140, 156, 147	syl2an2r 685	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
158	51, 149, 154, 155, 157	mulgcld 19035	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) ∈ 𝐵)
159	51, 52, 55, 13, 152, 47, 158, 31	gsummptres2 33000	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
160	31, 143	sstrd 3960	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ Word 𝐵)
161	160	sselda 3949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ Word 𝐵)
162	140, 161, 147	syl2an2r 685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
163	51, 149	mulg1 19020	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((mulGrp‘𝑅) Σg 𝑤))
164	162, 163	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((mulGrp‘𝑅) Σg 𝑤))
165	13	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → Word (𝐸 ∪ 𝐹) ∈ V)
166	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
167		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ 𝑇)
168		ind1 32787	. . . . . . . . . 10 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
169	165, 166, 167, 168	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
170	169	oveq1d 7405	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
171	140	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (mulGrp‘𝑅) ∈ Mnd)
172	75	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑃:𝐹⟶𝐵)
173	20	ad4ant13 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐹)
174	172, 173	ffvelcdmd 7060	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) ∈ 𝐵)
175	106	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃 supp 0 ) ⊆ 𝐵)
176	175, 92	sseldd 3950	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐵)
177	137, 64	mgpplusg 20060	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
178	146, 177	gsumws2 18776	. . . . . . . . . . 11 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ (𝑃‘𝑓) ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
179	171, 174, 176, 178	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
180		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
181	180	oveq2d 7406	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg 𝑤) = ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩))
182	91	fveq2d 6865	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘(𝑤‘1)) = (𝑃‘𝑓))
183	182, 91	oveq12d 7408	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((𝑃‘𝑓) · 𝑓))
184	179, 181, 183	3eqtr4rd 2776	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
185	184, 97	r19.29a 3142	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
186	164, 170, 185	3eqtr4d 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
187	186	mpteq2dva 5203	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1))))
188	187	oveq2d 7406	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
189	159, 188	eqtrd 2765	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
190	129, 130, 189	3eqtr4d 2775	. . 3 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
191	5, 50, 190	rspcedvdw 3594	. 2 ⊢ (𝜑 → ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
192		elrgspnsubrun.n	. . 3 ⊢ 𝑁 = (RingSpan‘𝑅)
193		breq1 5113	. . . 4 ⊢ (ℎ = 𝑖 → (ℎ finSupp 0 ↔ 𝑖 finSupp 0))
194	193	cbvrabv 3419	. . 3 ⊢ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0} = {𝑖 ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ 𝑖 finSupp 0}
195	51, 137, 149, 192, 194, 54, 141	elrgspn 33204	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)) ↔ ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
196	191, 195	mpbird 257	1 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  {crab 3408  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ⊆ wss 3917  {cpr 4594   class class class wbr 5110   ↦ cmpt 5191  ran crn 5642   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390   supp csupp 8142   ↑_m cmap 8802  Fincfn 8921   finSupp cfsupp 9319  0cc0 11075  1c1 11076  ℤcz 12536  Word cword 14485  ⟨“cs2 14814  Basecbs 17186  ._rcmulr 17228  0_gc0g 17409   Σ_g cgsu 17410  Mndcmnd 18668  Grpcgrp 18872  ._gcmg 19006  CMndccmn 19717  mulGrpcmgp 20056  Ringcrg 20149  CRingccrg 20150  SubRingcsubrg 20485  RingSpancrgspn 20526  𝟭cind 32780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-om 7846  df-1st 7971  df-2nd 7972  df-supp 8143  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9320  df-sup 9400  df-oi 9470  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-z 12537  df-dec 12657  df-uz 12801  df-rp 12959  df-fz 13476  df-fzo 13623  df-seq 13974  df-exp 14034  df-hash 14303  df-word 14486  df-concat 14543  df-s1 14568  df-substr 14613  df-pfx 14643  df-s2 14821  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15461  df-sum 15660  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-starv 17242  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-0g 17411  df-gsum 17412  df-mre 17554  df-mrc 17555  df-acs 17557  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-mhm 18717  df-submnd 18718  df-grp 18875  df-minusg 18876  df-mulg 19007  df-subg 19062  df-ghm 19152  df-cntz 19256  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-ring 20151  df-cring 20152  df-oppr 20253  df-subrng 20462  df-subrg 20486  df-rgspn 20527  df-cnfld 21272  df-zring 21364  df-ind 32781

This theorem is referenced by:  elrgspnsubrun  33207