Theorem elrgspnsubrunlem1 33206

Description: Lemma for elrgspnsubrun 33208, 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 6825	. . . . . . 7 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑔‘𝑤) = (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤))
2	1	oveq1d 7368	. . . . . 6 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
3	2	mpteq2dv 5189	. . . . 5 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))
4	3	oveq2d 7369	. . . 4 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
5	4	eqeq2d 2740	. . 3 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) ↔ 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
6		breq1 5098	. . . 4 ⊢ (ℎ = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (ℎ finSupp 0 ↔ ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0))
7		zex 12499	. . . . . 6 ⊢ ℤ ∈ V
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → ℤ ∈ V)
9		elrgspnsubrun.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))
10		elrgspnsubrun.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))
11	9, 10	unexd 7694	. . . . . 6 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ V)
12		wrdexg 14450	. . . . . 6 ⊢ ((𝐸 ∪ 𝐹) ∈ V → Word (𝐸 ∪ 𝐹) ∈ V)
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ∈ V)
14		elrgspnsubrunlem1.t	. . . . . . . 8 ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
15		ssun1 4131	. . . . . . . . . . . 12 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
16		elrgspnsubrunlem1.p1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:𝐹⟶𝐸)
17	16	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐸)
18		suppssdm 8117	. . . . . . . . . . . . . . 15 ⊢ (𝑃 supp 0 ) ⊆ dom 𝑃
19	18, 16	fssdm 6675	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐹)
20	19	sselda 3937	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ 𝐹)
21	17, 20	ffvelcdmd 7023	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ 𝐸)
22	15, 21	sselid 3935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ (𝐸 ∪ 𝐹))
23		ssun2 4132	. . . . . . . . . . . . 13 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
24	19, 23	sstrdi 3950	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ (𝐸 ∪ 𝐹))
25	24	sselda 3937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ (𝐸 ∪ 𝐹))
26	22, 25	s2cld 14797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
27	26	ralrimiva 3121	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
28		eqid 2729	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
29	28	rnmptss 7061	. . . . . . . . 9 ⊢ (∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹) → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
30	27, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
31	14, 30	eqsstrid 3976	. . . . . . 7 ⊢ (𝜑 → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
32		indf 32817	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
33	13, 31, 32	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
34		0zd 12502	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
35		1zzd 12525	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
36	34, 35	prssd 4776	. . . . . 6 ⊢ (𝜑 → {0, 1} ⊆ ℤ)
37	33, 36	fssd 6673	. . . . 5 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶ℤ)
38	8, 13, 37	elmapdd 8775	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)))
39	33	ffund 6660	. . . . 5 ⊢ (𝜑 → Fun ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇))
40		indsupp 32829	. . . . . . 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 9278	. . . . . . . 8 ⊢ (𝜑 → (𝑃 supp 0 ) ∈ Fin)
44		mptfi 9260	. . . . . . . 8 ⊢ ((𝑃 supp 0 ) ∈ Fin → (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
45		rnfi 9249	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
46	43, 44, 45	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
47	14, 46	eqeltrid 2832	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ Fin)
48	41, 47	eqeltrd 2828	. . . . 5 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) ∈ Fin)
49	38, 34, 39, 48	isfsuppd 9275	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0)
50	6, 38, 49	elrabd 3652	. . 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 20150	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
55	54	ringcmnd 20188	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
56	16	ffnd 6657	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 Fn 𝐹)
57	56	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑃 Fn 𝐹)
58	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝐹 ∈ (SubRing‘𝑅))
59	52	fvexi 6840	. . . . . . . . . 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 8111	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → (𝑃‘𝑒) = 0 )
63	62	oveq1d 7368	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = ( 0 · 𝑒))
64		elrgspnsubrun.t	. . . . . . . 8 ⊢ · = (.r‘𝑅)
65	54	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑅 ∈ Ring)
66	51	subrgss 20476	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubRing‘𝑅) → 𝐹 ⊆ 𝐵)
67	10, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
68	67	ssdifssd 4100	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∖ (𝑃 supp 0 )) ⊆ 𝐵)
69	68	sselda 3937	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ 𝐵)
70	51, 64, 52, 65, 69	ringlzd 20199	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ( 0 · 𝑒) = 0 )
71	63, 70	eqtrd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = 0 )
72	54	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑅 ∈ Ring)
73	51	subrgss 20476	. . . . . . . . . 10 ⊢ (𝐸 ∈ (SubRing‘𝑅) → 𝐸 ⊆ 𝐵)
74	9, 73	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝐵)
75	16, 74	fssd 6673	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐹⟶𝐵)
76	75	ffvelcdmda 7022	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → (𝑃‘𝑒) ∈ 𝐵)
77	67	sselda 3937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒 ∈ 𝐵)
78	51, 64, 72, 76, 77	ringcld 20164	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
79	51, 52, 55, 10, 71, 43, 78, 19	gsummptres2 33025	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))))
80		nfcv 2891	. . . . . 6 ⊢ Ⅎ𝑒((𝑃‘(𝑤‘1)) · (𝑤‘1))
81		fveq2 6826	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → (𝑃‘𝑒) = (𝑃‘(𝑤‘1)))
82		id 22	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → 𝑒 = (𝑤‘1))
83	81, 82	oveq12d 7371	. . . . . 6 ⊢ (𝑒 = (𝑤‘1) → ((𝑃‘𝑒) · 𝑒) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
84		ssidd 3961	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
85	19	sselda 3937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐹)
86	85, 78	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
87		fveq1 6825	. . . . . . . . . 10 ⊢ (𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩ → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
88	87	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
89		s2fv1 14814	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
90	89	ad2antlr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
91	88, 90	eqtrd 2764	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = 𝑓)
92		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ (𝑃 supp 0 ))
93	91, 92	eqeltrd 2828	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) ∈ (𝑃 supp 0 ))
94	14	eleq2i 2820	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
95	94	biimpi 216	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
96	95	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
97	28, 96	elrnmpt2d 5912	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
98	93, 97	r19.29a 3137	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝑤‘1) ∈ (𝑃 supp 0 ))
99		fveq2 6826	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → (𝑃‘𝑓) = (𝑃‘𝑒))
100		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → 𝑓 = 𝑒)
101	99, 100	s2eqd 14789	. . . . . . . . . 10 ⊢ (𝑓 = 𝑒 → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
102	101	cbvmptv 5199	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑒 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑒)𝑒”⟩)
103		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ (𝑃 supp 0 ))
104	75	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐵)
105	104, 85	ffvelcdmd 7023	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → (𝑃‘𝑒) ∈ 𝐵)
106	19, 67	sstrd 3948	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐵)
107	106	sselda 3937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐵)
108	105, 107	s2cld 14797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ Word 𝐵)
109	102, 103, 108	elrnmpt1d 5910	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
110	109, 14	eleqtrrdi 2839	. . . . . . 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 6828	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
114	89	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
115	112, 113, 114	3eqtrrd 2769	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 = 𝑒)
116	115	fveq2d 6830	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) = (𝑃‘𝑒))
117	116, 115	s2eqd 14789	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
118	111, 117	eqtrd 2764	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
119	97	ad4ant13 751	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
120	118, 119	r19.29a 3137	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
121		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
122	121	fveq1d 6828	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑒)𝑒”⟩‘1))
123		s2fv1 14814	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
124	123	ad3antlr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
125	122, 124	eqtr2d 2765	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑒 = (𝑤‘1))
126	120, 125	impbida 800	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) → (𝑒 = (𝑤‘1) ↔ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩))
127	110, 126	reu6dv 32436	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ∃!𝑤 ∈ 𝑇 𝑒 = (𝑤‘1))
128	80, 51, 52, 83, 55, 43, 84, 86, 98, 127	gsummptf1o 19861	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
129	79, 128	eqtrd 2764	. . . 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 32820	. . . . . . . . 9 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
135	131, 132, 133, 134	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
136	135	oveq1d 7368	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
137		eqid 2729	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
138	137	crngmgp 20145	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
139	53, 138	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
140	139	cmnmndd 19702	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
141	74, 67	unssd 4145	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ 𝐵)
142		sswrd 14448	. . . . . . . . . . . 12 ⊢ ((𝐸 ∪ 𝐹) ⊆ 𝐵 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
143	141, 142	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
144	143	ssdifssd 4100	. . . . . . . . . 10 ⊢ (𝜑 → (Word (𝐸 ∪ 𝐹) ∖ 𝑇) ⊆ Word 𝐵)
145	144	sselda 3937	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ Word 𝐵)
146	137, 51	mgpbas 20049	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
147	146	gsumwcl 18732	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
148	140, 145, 147	syl2an2r 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
149		eqid 2729	. . . . . . . . 9 ⊢ (.g‘𝑅) = (.g‘𝑅)
150	51, 52, 149	mulg0 18972	. . . . . . . 8 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
151	148, 150	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
152	136, 151	eqtrd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
153	53	crnggrpd 20151	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
154	153	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑅 ∈ Grp)
155	37	ffvelcdmda 7022	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) ∈ ℤ)
156	143	sselda 3937	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word 𝐵)
157	140, 156, 147	syl2an2r 685	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
158	51, 149, 154, 155, 157	mulgcld 18994	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) ∈ 𝐵)
159	51, 52, 55, 13, 152, 47, 158, 31	gsummptres2 33025	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
160	31, 143	sstrd 3948	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ Word 𝐵)
161	160	sselda 3937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ Word 𝐵)
162	140, 161, 147	syl2an2r 685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
163	51, 149	mulg1 18979	. . . . . . . . 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 32819	. . . . . . . . . 10 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
169	165, 166, 167, 168	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
170	169	oveq1d 7368	. . . . . . . 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 7023	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) ∈ 𝐵)
175	106	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃 supp 0 ) ⊆ 𝐵)
176	175, 92	sseldd 3938	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐵)
177	137, 64	mgpplusg 20048	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
178	146, 177	gsumws2 18735	. . . . . . . . . . 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 7369	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg 𝑤) = ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩))
182	91	fveq2d 6830	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘(𝑤‘1)) = (𝑃‘𝑓))
183	182, 91	oveq12d 7371	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((𝑃‘𝑓) · 𝑓))
184	179, 181, 183	3eqtr4rd 2775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
185	184, 97	r19.29a 3137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
186	164, 170, 185	3eqtr4d 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
187	186	mpteq2dva 5188	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1))))
188	187	oveq2d 7369	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
189	159, 188	eqtrd 2764	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
190	129, 130, 189	3eqtr4d 2774	. . 3 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
191	5, 50, 190	rspcedvdw 3582	. 2 ⊢ (𝜑 → ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
192		elrgspnsubrun.n	. . 3 ⊢ 𝑁 = (RingSpan‘𝑅)
193		breq1 5098	. . . 4 ⊢ (ℎ = 𝑖 → (ℎ finSupp 0 ↔ 𝑖 finSupp 0))
194	193	cbvrabv 3407	. . 3 ⊢ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0} = {𝑖 ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ 𝑖 finSupp 0}
195	51, 137, 149, 192, 194, 54, 141	elrgspn 33205	. 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 3044  ∃wrex 3053  {crab 3396  Vcvv 3438   ∖ cdif 3902   ∪ cun 3903   ⊆ wss 3905  {cpr 4581   class class class wbr 5095   ↦ cmpt 5176  ran crn 5624   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353   supp csupp 8100   ↑_m cmap 8760  Fincfn 8879   finSupp cfsupp 9270  0cc0 11028  1c1 11029  ℤcz 12490  Word cword 14439  ⟨“cs2 14767  Basecbs 17139  ._rcmulr 17181  0_gc0g 17362   Σ_g cgsu 17363  Mndcmnd 18627  Grpcgrp 18831  ._gcmg 18965  CMndccmn 19678  mulGrpcmgp 20044  Ringcrg 20137  CRingccrg 20138  SubRingcsubrg 20473  RingSpancrgspn 20514  𝟭cind 32812

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 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-inf2 9556  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106  ax-addf 11107

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-tpos 8166  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-map 8762  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-sup 9351  df-oi 9421  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-z 12491  df-dec 12611  df-uz 12755  df-rp 12913  df-fz 13430  df-fzo 13577  df-seq 13928  df-exp 13988  df-hash 14257  df-word 14440  df-concat 14497  df-s1 14522  df-substr 14567  df-pfx 14597  df-s2 14774  df-cj 15025  df-re 15026  df-im 15027  df-sqrt 15161  df-abs 15162  df-clim 15414  df-sum 15613  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17140  df-ress 17161  df-plusg 17193  df-mulr 17194  df-starv 17195  df-tset 17199  df-ple 17200  df-ds 17202  df-unif 17203  df-0g 17364  df-gsum 17365  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18533  df-sgrp 18612  df-mnd 18628  df-mhm 18676  df-submnd 18677  df-grp 18834  df-minusg 18835  df-mulg 18966  df-subg 19021  df-ghm 19111  df-cntz 19215  df-cmn 19680  df-abl 19681  df-mgp 20045  df-rng 20057  df-ur 20086  df-ring 20139  df-cring 20140  df-oppr 20241  df-subrng 20450  df-subrg 20474  df-rgspn 20515  df-cnfld 21281  df-zring 21373  df-ind 32813

This theorem is referenced by:  elrgspnsubrun  33208