Theorem elrgspnsubrunlem1 33332

Description: Lemma for elrgspnsubrun 33334, 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 6830	. . . . . . 7 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑔‘𝑤) = (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤))
2	1	oveq1d 7375	. . . . . 6 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
3	2	mpteq2dv 5169	. . . . 5 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))
4	3	oveq2d 7376	. . . 4 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
5	4	eqeq2d 2752	. . 3 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) ↔ 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
6		breq1 5078	. . . 4 ⊢ (ℎ = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (ℎ finSupp 0 ↔ ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0))
7		zex 12528	. . . . . 6 ⊢ ℤ ∈ V
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → ℤ ∈ V)
9		elrgspnsubrun.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))
10		elrgspnsubrun.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))
11	9, 10	unexd 7701	. . . . . 6 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ V)
12		wrdexg 14481	. . . . . 6 ⊢ ((𝐸 ∪ 𝐹) ∈ V → Word (𝐸 ∪ 𝐹) ∈ V)
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ∈ V)
14		elrgspnsubrunlem1.t	. . . . . . . 8 ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
15		ssun1 4110	. . . . . . . . . . . 12 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
16		elrgspnsubrunlem1.p1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:𝐹⟶𝐸)
17	16	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐸)
18		suppssdm 8121	. . . . . . . . . . . . . . 15 ⊢ (𝑃 supp 0 ) ⊆ dom 𝑃
19	18, 16	fssdm 6678	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐹)
20	19	sselda 3917	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ 𝐹)
21	17, 20	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ 𝐸)
22	15, 21	sselid 3915	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ (𝐸 ∪ 𝐹))
23		ssun2 4111	. . . . . . . . . . . . 13 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
24	19, 23	sstrdi 3929	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ (𝐸 ∪ 𝐹))
25	24	sselda 3917	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ (𝐸 ∪ 𝐹))
26	22, 25	s2cld 14828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
27	26	ralrimiva 3133	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
28		eqid 2741	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
29	28	rnmptss 7068	. . . . . . . . 9 ⊢ (∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹) → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
30	27, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
31	14, 30	eqsstrid 3955	. . . . . . 7 ⊢ (𝜑 → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
32		indf 12160	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
33	13, 31, 32	syl2anc 591	. . . . . 6 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
34		0zd 12531	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
35		1zzd 12553	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
36	34, 35	prssd 4756	. . . . . 6 ⊢ (𝜑 → {0, 1} ⊆ ℤ)
37	33, 36	fssd 6676	. . . . 5 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶ℤ)
38	8, 13, 37	elmapdd 8782	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)))
39	33	ffund 6663	. . . . 5 ⊢ (𝜑 → Fun ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇))
40		indsupp 32950	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
41	13, 31, 40	syl2anc 591	. . . . . 6 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
42		elrgspnsubrunlem1.p2	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp 0 )
43	42	fsuppimpd 9276	. . . . . . . 8 ⊢ (𝜑 → (𝑃 supp 0 ) ∈ Fin)
44		mptfi 9255	. . . . . . . 8 ⊢ ((𝑃 supp 0 ) ∈ Fin → (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
45		rnfi 9244	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
46	43, 44, 45	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
47	14, 46	eqeltrid 2845	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ Fin)
48	41, 47	eqeltrd 2841	. . . . 5 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) ∈ Fin)
49	38, 34, 39, 48	isfsuppd 9273	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0)
50	6, 38, 49	elrabd 3633	. . 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 20222	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
55	54	ringcmnd 20260	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
56	16	ffnd 6660	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 Fn 𝐹)
57	56	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑃 Fn 𝐹)
58	10	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝐹 ∈ (SubRing‘𝑅))
59	52	fvexi 6845	. . . . . . . . . 10 ⊢ 0 ∈ V
60	59	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 0 ∈ V)
61		simpr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 )))
62	57, 58, 60, 61	fvdifsupp 8115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → (𝑃‘𝑒) = 0 )
63	62	oveq1d 7375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = ( 0 · 𝑒))
64		elrgspnsubrun.t	. . . . . . . 8 ⊢ · = (.r‘𝑅)
65	54	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑅 ∈ Ring)
66	51	subrgss 20548	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubRing‘𝑅) → 𝐹 ⊆ 𝐵)
67	10, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
68	67	ssdifssd 4080	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∖ (𝑃 supp 0 )) ⊆ 𝐵)
69	68	sselda 3917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ 𝐵)
70	51, 64, 52, 65, 69	ringlzd 20271	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ( 0 · 𝑒) = 0 )
71	63, 70	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = 0 )
72	54	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑅 ∈ Ring)
73	51	subrgss 20548	. . . . . . . . . 10 ⊢ (𝐸 ∈ (SubRing‘𝑅) → 𝐸 ⊆ 𝐵)
74	9, 73	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝐵)
75	16, 74	fssd 6676	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐹⟶𝐵)
76	75	ffvelcdmda 7029	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → (𝑃‘𝑒) ∈ 𝐵)
77	67	sselda 3917	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒 ∈ 𝐵)
78	51, 64, 72, 76, 77	ringcld 20236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
79	51, 52, 55, 10, 71, 43, 78, 19	gsummptres2 33138	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))))
80		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑒((𝑃‘(𝑤‘1)) · (𝑤‘1))
81		fveq2 6831	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → (𝑃‘𝑒) = (𝑃‘(𝑤‘1)))
82		id 22	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → 𝑒 = (𝑤‘1))
83	81, 82	oveq12d 7378	. . . . . 6 ⊢ (𝑒 = (𝑤‘1) → ((𝑃‘𝑒) · 𝑒) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
84		ssidd 3940	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
85	19	sselda 3917	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐹)
86	85, 78	syldan 598	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
87		fveq1 6830	. . . . . . . . . 10 ⊢ (𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩ → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
88	87	adantl 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
89		s2fv1 14845	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
90	89	ad2antlr 734	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
91	88, 90	eqtrd 2776	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = 𝑓)
92		simplr 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ (𝑃 supp 0 ))
93	91, 92	eqeltrd 2841	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) ∈ (𝑃 supp 0 ))
94	14	eleq2i 2833	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
95	94	bilani 506	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
96	28, 95	elrnmpt2d 5915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
97	93, 96	r19.29a 3149	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝑤‘1) ∈ (𝑃 supp 0 ))
98		fveq2 6831	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → (𝑃‘𝑓) = (𝑃‘𝑒))
99		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → 𝑓 = 𝑒)
100	98, 99	s2eqd 14820	. . . . . . . . . 10 ⊢ (𝑓 = 𝑒 → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
101	100	cbvmptv 5179	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑒 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑒)𝑒”⟩)
102		simpr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ (𝑃 supp 0 ))
103	75	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐵)
104	103, 85	ffvelcdmd 7030	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → (𝑃‘𝑒) ∈ 𝐵)
105	19, 67	sstrd 3927	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐵)
106	105	sselda 3917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐵)
107	104, 106	s2cld 14828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ Word 𝐵)
108	101, 102, 107	elrnmpt1d 5913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
109	108, 14	eleqtrrdi 2852	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ 𝑇)
110		simpr 486	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
111	82	ad3antlr 738	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑒 = (𝑤‘1))
112	110	fveq1d 6833	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
113	89	ad2antlr 734	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
114	111, 112, 113	3eqtrrd 2781	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 = 𝑒)
115	114	fveq2d 6835	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) = (𝑃‘𝑒))
116	115, 114	s2eqd 14820	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
117	110, 116	eqtrd 2776	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
118	96	ad4ant13 758	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
119	117, 118	r19.29a 3149	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
120		simpr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
121	120	fveq1d 6833	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑒)𝑒”⟩‘1))
122		s2fv1 14845	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
123	122	ad3antlr 738	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
124	121, 123	eqtr2d 2777	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑒 = (𝑤‘1))
125	119, 124	impbida 807	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) → (𝑒 = (𝑤‘1) ↔ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩))
126	109, 125	reu6dv 32564	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ∃!𝑤 ∈ 𝑇 𝑒 = (𝑤‘1))
127	80, 51, 52, 83, 55, 43, 84, 86, 97, 126	gsummptf1o 19933	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
128	79, 127	eqtrd 2776	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
129		elrgspnsubrunlem1.x	. . . 4 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))))
130	13	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → Word (𝐸 ∪ 𝐹) ∈ V)
131	31	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
132		simpr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇))
133		ind0 12164	. . . . . . . . 9 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
134	130, 131, 132, 133	syl3anc 1380	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
135	134	oveq1d 7375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
136		eqid 2741	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
137	136	crngmgp 20217	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
138	53, 137	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
139	138	cmnmndd 19774	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
140	74, 67	unssd 4124	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ 𝐵)
141		sswrd 14479	. . . . . . . . . . . 12 ⊢ ((𝐸 ∪ 𝐹) ⊆ 𝐵 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
142	140, 141	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
143	142	ssdifssd 4080	. . . . . . . . . 10 ⊢ (𝜑 → (Word (𝐸 ∪ 𝐹) ∖ 𝑇) ⊆ Word 𝐵)
144	143	sselda 3917	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ Word 𝐵)
145	136, 51	mgpbas 20121	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
146	145	gsumwcl 18802	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
147	139, 144, 146	syl2an2r 692	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
148		eqid 2741	. . . . . . . . 9 ⊢ (.g‘𝑅) = (.g‘𝑅)
149	51, 52, 148	mulg0 19045	. . . . . . . 8 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
150	147, 149	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
151	135, 150	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
152	53	crnggrpd 20223	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
153	152	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑅 ∈ Grp)
154	37	ffvelcdmda 7029	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) ∈ ℤ)
155	142	sselda 3917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word 𝐵)
156	139, 155, 146	syl2an2r 692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
157	51, 148, 153, 154, 156	mulgcld 19067	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) ∈ 𝐵)
158	51, 52, 55, 13, 151, 47, 157, 31	gsummptres2 33138	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
159	31, 142	sstrd 3927	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ Word 𝐵)
160	159	sselda 3917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ Word 𝐵)
161	139, 160, 146	syl2an2r 692	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
162	51, 148	mulg1 19052	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((mulGrp‘𝑅) Σg 𝑤))
163	161, 162	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((mulGrp‘𝑅) Σg 𝑤))
164	13	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → Word (𝐸 ∪ 𝐹) ∈ V)
165	31	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
166		simpr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ 𝑇)
167		ind1 12163	. . . . . . . . . 10 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
168	164, 165, 166, 167	syl3anc 1380	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
169	168	oveq1d 7375	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
170	139	ad3antrrr 737	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (mulGrp‘𝑅) ∈ Mnd)
171	75	ad3antrrr 737	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑃:𝐹⟶𝐵)
172	20	ad4ant13 758	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐹)
173	171, 172	ffvelcdmd 7030	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) ∈ 𝐵)
174	105	ad3antrrr 737	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃 supp 0 ) ⊆ 𝐵)
175	174, 92	sseldd 3918	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐵)
176	136, 64	mgpplusg 20120	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
177	145, 176	gsumws2 18805	. . . . . . . . . . 11 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ (𝑃‘𝑓) ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
178	170, 173, 175, 177	syl3anc 1380	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
179		simpr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
180	179	oveq2d 7376	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg 𝑤) = ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩))
181	91	fveq2d 6835	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘(𝑤‘1)) = (𝑃‘𝑓))
182	181, 91	oveq12d 7378	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((𝑃‘𝑓) · 𝑓))
183	178, 180, 182	3eqtr4rd 2787	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
184	183, 96	r19.29a 3149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
185	163, 169, 184	3eqtr4d 2786	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
186	185	mpteq2dva 5168	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1))))
187	186	oveq2d 7376	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
188	158, 187	eqtrd 2776	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
189	128, 129, 188	3eqtr4d 2786	. . 3 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
190	5, 50, 189	rspcedvdw 3565	. 2 ⊢ (𝜑 → ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
191		elrgspnsubrun.n	. . 3 ⊢ 𝑁 = (RingSpan‘𝑅)
192		breq1 5078	. . . 4 ⊢ (ℎ = 𝑖 → (ℎ finSupp 0 ↔ 𝑖 finSupp 0))
193	192	cbvrabv 3403	. . 3 ⊢ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0} = {𝑖 ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ 𝑖 finSupp 0}
194	51, 136, 148, 191, 193, 54, 140	elrgspn 33331	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)) ↔ ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
195	190, 194	mpbird 259	1 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065  {crab 3393  Vcvv 3433   ∖ cdif 3882   ∪ cun 3883   ⊆ wss 3885  {cpr 4560   class class class wbr 5075   ↦ cmpt 5156  ran crn 5622   Fn wfn 6484  ⟶wf 6485  ‘cfv 6489  (class class class)co 7360   supp csupp 8104   ↑_m cmap 8767  Fincfn 8887   finSupp cfsupp 9268  0cc0 11033  1c1 11034  𝟭cind 12154  ℤcz 12519  Word cword 14470  ⟨“cs2 14798  Basecbs 17174  ._rcmulr 17216  0_gc0g 17397   Σ_g cgsu 17398  Mndcmnd 18697  Grpcgrp 18904  ._gcmg 19038  CMndccmn 19750  mulGrpcmgp 20116  Ringcrg 20209  CRingccrg 20210  SubRingcsubrg 20545  RingSpancrgspn 20586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-inf2 9557  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-pre-sup 11111  ax-addf 11112

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-iin 4927  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8105  df-tpos 8170  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-sup 9349  df-oi 9419  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-ind 12155  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-rp 12938  df-fz 13457  df-fzo 13604  df-seq 13959  df-exp 14019  df-hash 14288  df-word 14471  df-concat 14528  df-s1 14554  df-substr 14599  df-pfx 14629  df-s2 14805  df-cj 15056  df-re 15057  df-im 15058  df-sqrt 15192  df-abs 15193  df-clim 15445  df-sum 15644  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-starv 17230  df-tset 17234  df-ple 17235  df-ds 17237  df-unif 17238  df-0g 17399  df-gsum 17400  df-mre 17543  df-mrc 17544  df-acs 17546  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18746  df-submnd 18747  df-grp 18907  df-minusg 18908  df-mulg 19039  df-subg 19094  df-ghm 19183  df-cntz 19287  df-cmn 19752  df-abl 19753  df-mgp 20117  df-rng 20129  df-ur 20158  df-ring 20211  df-cring 20212  df-oppr 20312  df-subrng 20522  df-subrg 20546  df-rgspn 20587  df-cnfld 21352  df-zring 21426

This theorem is referenced by:  elrgspnsubrun  33334