Theorem elrgspnsubrunlem1 33341

Description: Lemma for elrgspnsubrun 33343, 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 6841	. . . . . . 7 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑔‘𝑤) = (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤))
2	1	oveq1d 7383	. . . . . 6 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
3	2	mpteq2dv 5194	. . . . 5 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))
4	3	oveq2d 7384	. . . 4 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
5	4	eqeq2d 2748	. . 3 ⊢ (𝑔 = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) ↔ 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
6		breq1 5103	. . . 4 ⊢ (ℎ = ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) → (ℎ finSupp 0 ↔ ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) finSupp 0))
7		zex 12509	. . . . . 6 ⊢ ℤ ∈ V
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → ℤ ∈ V)
9		elrgspnsubrun.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (SubRing‘𝑅))
10		elrgspnsubrun.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝑅))
11	9, 10	unexd 7709	. . . . . 6 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ V)
12		wrdexg 14459	. . . . . 6 ⊢ ((𝐸 ∪ 𝐹) ∈ V → Word (𝐸 ∪ 𝐹) ∈ V)
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ∈ V)
14		elrgspnsubrunlem1.t	. . . . . . . 8 ⊢ 𝑇 = ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
15		ssun1 4132	. . . . . . . . . . . 12 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
16		elrgspnsubrunlem1.p1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃:𝐹⟶𝐸)
17	16	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐸)
18		suppssdm 8129	. . . . . . . . . . . . . . 15 ⊢ (𝑃 supp 0 ) ⊆ dom 𝑃
19	18, 16	fssdm 6689	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐹)
20	19	sselda 3935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ 𝐹)
21	17, 20	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ 𝐸)
22	15, 21	sselid 3933	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → (𝑃‘𝑓) ∈ (𝐸 ∪ 𝐹))
23		ssun2 4133	. . . . . . . . . . . . 13 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
24	19, 23	sstrdi 3948	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ (𝐸 ∪ 𝐹))
25	24	sselda 3935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → 𝑓 ∈ (𝐸 ∪ 𝐹))
26	22, 25	s2cld 14806	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
27	26	ralrimiva 3130	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹))
28		eqid 2737	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩)
29	28	rnmptss 7077	. . . . . . . . 9 ⊢ (∀𝑓 ∈ (𝑃 supp 0 )⟨“(𝑃‘𝑓)𝑓”⟩ ∈ Word (𝐸 ∪ 𝐹) → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
30	27, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ⊆ Word (𝐸 ∪ 𝐹))
31	14, 30	eqsstrid 3974	. . . . . . 7 ⊢ (𝜑 → 𝑇 ⊆ Word (𝐸 ∪ 𝐹))
32		indf 32945	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
33	13, 31, 32	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶{0, 1})
34		0zd 12512	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
35		1zzd 12534	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
36	34, 35	prssd 4780	. . . . . 6 ⊢ (𝜑 → {0, 1} ⊆ ℤ)
37	33, 36	fssd 6687	. . . . 5 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇):Word (𝐸 ∪ 𝐹)⟶ℤ)
38	8, 13, 37	elmapdd 8790	. . . 4 ⊢ (𝜑 → ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)))
39	33	ffund 6674	. . . . 5 ⊢ (𝜑 → Fun ((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇))
40		indsupp 32960	. . . . . . 7 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
41	13, 31, 40	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) = 𝑇)
42		elrgspnsubrunlem1.p2	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp 0 )
43	42	fsuppimpd 9284	. . . . . . . 8 ⊢ (𝜑 → (𝑃 supp 0 ) ∈ Fin)
44		mptfi 9263	. . . . . . . 8 ⊢ ((𝑃 supp 0 ) ∈ Fin → (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
45		rnfi 9252	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
46	43, 44, 45	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) ∈ Fin)
47	14, 46	eqeltrid 2841	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ Fin)
48	41, 47	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇) supp 0) ∈ Fin)
49	38, 34, 39, 48	isfsuppd 9281	. . . 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 20193	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
55	54	ringcmnd 20231	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
56	16	ffnd 6671	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 Fn 𝐹)
57	56	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑃 Fn 𝐹)
58	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝐹 ∈ (SubRing‘𝑅))
59	52	fvexi 6856	. . . . . . . . . 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 8123	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → (𝑃‘𝑒) = 0 )
63	62	oveq1d 7383	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = ( 0 · 𝑒))
64		elrgspnsubrun.t	. . . . . . . 8 ⊢ · = (.r‘𝑅)
65	54	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑅 ∈ Ring)
66	51	subrgss 20517	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubRing‘𝑅) → 𝐹 ⊆ 𝐵)
67	10, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
68	67	ssdifssd 4101	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∖ (𝑃 supp 0 )) ⊆ 𝐵)
69	68	sselda 3935	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → 𝑒 ∈ 𝐵)
70	51, 64, 52, 65, 69	ringlzd 20242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ( 0 · 𝑒) = 0 )
71	63, 70	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝐹 ∖ (𝑃 supp 0 ))) → ((𝑃‘𝑒) · 𝑒) = 0 )
72	54	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑅 ∈ Ring)
73	51	subrgss 20517	. . . . . . . . . 10 ⊢ (𝐸 ∈ (SubRing‘𝑅) → 𝐸 ⊆ 𝐵)
74	9, 73	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝐵)
75	16, 74	fssd 6687	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐹⟶𝐵)
76	75	ffvelcdmda 7038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → (𝑃‘𝑒) ∈ 𝐵)
77	67	sselda 3935	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒 ∈ 𝐵)
78	51, 64, 72, 76, 77	ringcld 20207	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
79	51, 52, 55, 10, 71, 43, 78, 19	gsummptres2 33147	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ 𝐹 ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))))
80		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑒((𝑃‘(𝑤‘1)) · (𝑤‘1))
81		fveq2 6842	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → (𝑃‘𝑒) = (𝑃‘(𝑤‘1)))
82		id 22	. . . . . . 7 ⊢ (𝑒 = (𝑤‘1) → 𝑒 = (𝑤‘1))
83	81, 82	oveq12d 7386	. . . . . 6 ⊢ (𝑒 = (𝑤‘1) → ((𝑃‘𝑒) · 𝑒) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
84		ssidd 3959	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
85	19	sselda 3935	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐹)
86	85, 78	syldan 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ((𝑃‘𝑒) · 𝑒) ∈ 𝐵)
87		fveq1 6841	. . . . . . . . . 10 ⊢ (𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩ → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
88	87	adantl 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
89		s2fv1 14823	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
90	89	ad2antlr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
91	88, 90	eqtrd 2772	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = 𝑓)
92		simplr 769	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ (𝑃 supp 0 ))
93	91, 92	eqeltrd 2837	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) ∈ (𝑃 supp 0 ))
94	14	eleq2i 2829	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑇 ↔ 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
95	94	biimpi 216	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑇 → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
96	95	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
97	28, 96	elrnmpt2d 5923	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
98	93, 97	r19.29a 3146	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (𝑤‘1) ∈ (𝑃 supp 0 ))
99		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → (𝑃‘𝑓) = (𝑃‘𝑒))
100		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑒 → 𝑓 = 𝑒)
101	99, 100	s2eqd 14798	. . . . . . . . . 10 ⊢ (𝑓 = 𝑒 → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
102	101	cbvmptv 5204	. . . . . . . . 9 ⊢ (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩) = (𝑒 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑒)𝑒”⟩)
103		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ (𝑃 supp 0 ))
104	75	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑃:𝐹⟶𝐵)
105	104, 85	ffvelcdmd 7039	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → (𝑃‘𝑒) ∈ 𝐵)
106	19, 67	sstrd 3946	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 supp 0 ) ⊆ 𝐵)
107	106	sselda 3935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → 𝑒 ∈ 𝐵)
108	105, 107	s2cld 14806	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ Word 𝐵)
109	102, 103, 108	elrnmpt1d 5921	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ ran (𝑓 ∈ (𝑃 supp 0 ) ↦ ⟨“(𝑃‘𝑓)𝑓”⟩))
110	109, 14	eleqtrrdi 2848	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ⟨“(𝑃‘𝑒)𝑒”⟩ ∈ 𝑇)
111		simpr 484	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
112	82	ad3antlr 732	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑒 = (𝑤‘1))
113	111	fveq1d 6844	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑓)𝑓”⟩‘1))
114	89	ad2antlr 728	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (⟨“(𝑃‘𝑓)𝑓”⟩‘1) = 𝑓)
115	112, 113, 114	3eqtrrd 2777	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 = 𝑒)
116	115	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) = (𝑃‘𝑒))
117	116, 115	s2eqd 14798	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ⟨“(𝑃‘𝑓)𝑓”⟩ = ⟨“(𝑃‘𝑒)𝑒”⟩)
118	111, 117	eqtrd 2772	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
119	97	ad4ant13 752	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → ∃𝑓 ∈ (𝑃 supp 0 )𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
120	118, 119	r19.29a 3146	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑒 = (𝑤‘1)) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
121		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩)
122	121	fveq1d 6844	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (𝑤‘1) = (⟨“(𝑃‘𝑒)𝑒”⟩‘1))
123		s2fv1 14823	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑃 supp 0 ) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
124	123	ad3antlr 732	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → (⟨“(𝑃‘𝑒)𝑒”⟩‘1) = 𝑒)
125	122, 124	eqtr2d 2773	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) ∧ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩) → 𝑒 = (𝑤‘1))
126	120, 125	impbida 801	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) ∧ 𝑤 ∈ 𝑇) → (𝑒 = (𝑤‘1) ↔ 𝑤 = ⟨“(𝑃‘𝑒)𝑒”⟩))
127	110, 126	reu6dv 32559	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ (𝑃 supp 0 )) → ∃!𝑤 ∈ 𝑇 𝑒 = (𝑤‘1))
128	80, 51, 52, 83, 55, 43, 84, 86, 98, 127	gsummptf1o 19904	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑒 ∈ (𝑃 supp 0 ) ↦ ((𝑃‘𝑒) · 𝑒))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
129	79, 128	eqtrd 2772	. . . 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 32948	. . . . . . . . 9 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
135	131, 132, 133, 134	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 0)
136	135	oveq1d 7383	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
137		eqid 2737	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
138	137	crngmgp 20188	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
139	53, 138	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
140	139	cmnmndd 19745	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
141	74, 67	unssd 4146	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ 𝐵)
142		sswrd 14457	. . . . . . . . . . . 12 ⊢ ((𝐸 ∪ 𝐹) ⊆ 𝐵 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
143	141, 142	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word 𝐵)
144	143	ssdifssd 4101	. . . . . . . . . 10 ⊢ (𝜑 → (Word (𝐸 ∪ 𝐹) ∖ 𝑇) ⊆ Word 𝐵)
145	144	sselda 3935	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → 𝑤 ∈ Word 𝐵)
146	137, 51	mgpbas 20092	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
147	146	gsumwcl 18776	. . . . . . . . 9 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
148	140, 145, 147	syl2an2r 686	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
149		eqid 2737	. . . . . . . . 9 ⊢ (.g‘𝑅) = (.g‘𝑅)
150	51, 52, 149	mulg0 19016	. . . . . . . 8 ⊢ (((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵 → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
151	148, 150	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → (0(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
152	136, 151	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (Word (𝐸 ∪ 𝐹) ∖ 𝑇)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = 0 )
153	53	crnggrpd 20194	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
154	153	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑅 ∈ Grp)
155	37	ffvelcdmda 7038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) ∈ ℤ)
156	143	sselda 3935	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word 𝐵)
157	140, 156, 147	syl2an2r 686	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
158	51, 149, 154, 155, 157	mulgcld 19038	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) ∈ 𝐵)
159	51, 52, 55, 13, 152, 47, 158, 31	gsummptres2 33147	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
160	31, 143	sstrd 3946	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ Word 𝐵)
161	160	sselda 3935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → 𝑤 ∈ Word 𝐵)
162	140, 161, 147	syl2an2r 686	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((mulGrp‘𝑅) Σg 𝑤) ∈ 𝐵)
163	51, 149	mulg1 19023	. . . . . . . . 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 32947	. . . . . . . . . 10 ⊢ ((Word (𝐸 ∪ 𝐹) ∈ V ∧ 𝑇 ⊆ Word (𝐸 ∪ 𝐹) ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
169	165, 166, 167, 168	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → (((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤) = 1)
170	169	oveq1d 7383	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = (1(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))
171	140	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (mulGrp‘𝑅) ∈ Mnd)
172	75	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑃:𝐹⟶𝐵)
173	20	ad4ant13 752	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐹)
174	172, 173	ffvelcdmd 7039	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘𝑓) ∈ 𝐵)
175	106	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃 supp 0 ) ⊆ 𝐵)
176	175, 92	sseldd 3936	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑓 ∈ 𝐵)
177	137, 64	mgpplusg 20091	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
178	146, 177	gsumws2 18779	. . . . . . . . . . 11 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ (𝑃‘𝑓) ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
179	171, 174, 176, 178	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩) = ((𝑃‘𝑓) · 𝑓))
180		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩)
181	180	oveq2d 7384	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((mulGrp‘𝑅) Σg 𝑤) = ((mulGrp‘𝑅) Σg ⟨“(𝑃‘𝑓)𝑓”⟩))
182	91	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → (𝑃‘(𝑤‘1)) = (𝑃‘𝑓))
183	182, 91	oveq12d 7386	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((𝑃‘𝑓) · 𝑓))
184	179, 181, 183	3eqtr4rd 2783	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑇) ∧ 𝑓 ∈ (𝑃 supp 0 )) ∧ 𝑤 = ⟨“(𝑃‘𝑓)𝑓”⟩) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
185	184, 97	r19.29a 3146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((𝑃‘(𝑤‘1)) · (𝑤‘1)) = ((mulGrp‘𝑅) Σg 𝑤))
186	164, 170, 185	3eqtr4d 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑇) → ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)) = ((𝑃‘(𝑤‘1)) · (𝑤‘1)))
187	186	mpteq2dva 5193	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))) = (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1))))
188	187	oveq2d 7384	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
189	159, 188	eqtrd 2772	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ 𝑇 ↦ ((𝑃‘(𝑤‘1)) · (𝑤‘1)))))
190	129, 130, 189	3eqtr4d 2782	. . 3 ⊢ (𝜑 → 𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((((𝟭‘Word (𝐸 ∪ 𝐹))‘𝑇)‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
191	5, 50, 190	rspcedvdw 3581	. 2 ⊢ (𝜑 → ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤)))))
192		elrgspnsubrun.n	. . 3 ⊢ 𝑁 = (RingSpan‘𝑅)
193		breq1 5103	. . . 4 ⊢ (ℎ = 𝑖 → (ℎ finSupp 0 ↔ 𝑖 finSupp 0))
194	193	cbvrabv 3411	. . 3 ⊢ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0} = {𝑖 ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ 𝑖 finSupp 0}
195	51, 137, 149, 192, 194, 54, 141	elrgspn 33340	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)) ↔ ∃𝑔 ∈ {ℎ ∈ (ℤ ↑m Word (𝐸 ∪ 𝐹)) ∣ ℎ finSupp 0}𝑋 = (𝑅 Σg (𝑤 ∈ Word (𝐸 ∪ 𝐹) ↦ ((𝑔‘𝑤)(.g‘𝑅)((mulGrp‘𝑅) Σg 𝑤))))))
196	191, 195	mpbird 257	1 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐸 ∪ 𝐹)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ⊆ wss 3903  {cpr 4584   class class class wbr 5100   ↦ cmpt 5181  ran crn 5633   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368   supp csupp 8112   ↑_m cmap 8775  Fincfn 8895   finSupp cfsupp 9276  0cc0 11038  1c1 11039  ℤcz 12500  Word cword 14448  ⟨“cs2 14776  Basecbs 17148  ._rcmulr 17190  0_gc0g 17371   Σ_g cgsu 17372  Mndcmnd 18671  Grpcgrp 18875  ._gcmg 19009  CMndccmn 19721  mulGrpcmgp 20087  Ringcrg 20180  CRingccrg 20181  SubRingcsubrg 20514  RingSpancrgspn 20555  𝟭cind 32940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-sup 9357  df-oi 9427  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-z 12501  df-dec 12620  df-uz 12764  df-rp 12918  df-fz 13436  df-fzo 13583  df-seq 13937  df-exp 13997  df-hash 14266  df-word 14449  df-concat 14506  df-s1 14532  df-substr 14577  df-pfx 14607  df-s2 14783  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-clim 15423  df-sum 15622  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-tset 17208  df-ple 17209  df-ds 17211  df-unif 17212  df-0g 17373  df-gsum 17374  df-mre 17517  df-mrc 17518  df-acs 17520  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-grp 18878  df-minusg 18879  df-mulg 19010  df-subg 19065  df-ghm 19154  df-cntz 19258  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-ring 20182  df-cring 20183  df-oppr 20285  df-subrng 20491  df-subrg 20515  df-rgspn 20556  df-cnfld 21322  df-zring 21414  df-ind 32941

This theorem is referenced by:  elrgspnsubrun  33343