elrgspn

Description: Membership in the subring generated by the subset A . An element X lies in that subring if and only if X is a linear combination with integer coefficients of products of elements of A . (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	elrgspn.b	$⊢ B = {Base}_{R}$
	elrgspn.m	$⊢ M = {mulGrp}_{R}$
	elrgspn.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	elrgspn.n	$⊢ N = RingSpan (R)$
	elrgspn.f	$⊢ F = \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
	elrgspn.r	$⊢ φ \to R \in Ring$
	elrgspn.a	$⊢ φ \to A \subseteq B$
Assertion	elrgspn	$⊢ φ \to (X \in N (A) \leftrightarrow \exists g \in F X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$

Proof

Step	Hyp	Ref	Expression
1		elrgspn.b	$⊢ B = {Base}_{R}$
2		elrgspn.m	$⊢ M = {mulGrp}_{R}$
3		elrgspn.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		elrgspn.n	$⊢ N = RingSpan (R)$
5		elrgspn.f	$⊢ F = \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
6		elrgspn.r	$⊢ φ \to R \in Ring$
7		elrgspn.a	$⊢ φ \to A \subseteq B$
8	1	a1i	$⊢ φ \to B = {Base}_{R}$
9	4	a1i	$⊢ φ \to N = RingSpan (R)$
10		eqidd	$⊢ φ \to N (A) = N (A)$
11	6 8 7 9 10	rgspncl	$⊢ φ \to N (A) \in SubRing (R)$
12	1	subrgss	$⊢ N (A) \in SubRing (R) \to N (A) \subseteq B$
13	11 12	syl	$⊢ φ \to N (A) \subseteq B$
14	13	sselda	$⊢ (φ \land X \in N (A)) \to X \in B$
15		simpr	$⊢ ((φ \land g \in F) \land X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	6	ringcmnd	$⊢ φ \to R \in CMnd$
18	17	adantr	$⊢ (φ \land g \in F) \to R \in CMnd$
19	1	fvexi	$⊢ B \in V$
20	19	a1i	$⊢ φ \to B \in V$
21	20 7	ssexd	$⊢ φ \to A \in V$
22	21	adantr	$⊢ (φ \land g \in F) \to A \in V$
23		wrdexg	$⊢ A \in V \to Word A \in V$
24	22 23	syl	$⊢ (φ \land g \in F) \to Word A \in V$
25	6	ringgrpd	$⊢ φ \to R \in Grp$
26	25	ad2antrr	$⊢ ((φ \land g \in F) \land w \in Word A) \to R \in Grp$
27		breq1	$⊢ f = g \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (g))$
28	27 5	elrab2	$⊢ g \in F \leftrightarrow (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
29	28	biimpi	$⊢ g \in F \to (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
30	29	simpld	$⊢ g \in F \to g \in (ℤ^{Word A})$
31	30	adantl	$⊢ (φ \land g \in F) \to g \in (ℤ^{Word A})$
32	31	elmaprd	$⊢ (φ \land g \in F) \to g : Word A ⟶ ℤ$
33	32	ffvelcdmda	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \in ℤ$
34	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
35	6 34	syl	$⊢ φ \to M \in Mnd$
36	35	ad2antrr	$⊢ ((φ \land g \in F) \land w \in Word A) \to M \in Mnd$
37		sswrd	$⊢ A \subseteq B \to Word A \subseteq Word B$
38	7 37	syl	$⊢ φ \to Word A \subseteq Word B$
39	38	adantr	$⊢ (φ \land g \in F) \to Word A \subseteq Word B$
40	39	sselda	$⊢ ((φ \land g \in F) \land w \in Word A) \to w \in Word B$
41	2 1	mgpbas	$⊢ B = {Base}_{M}$
42	41	gsumwcl	$⊢ (M \in Mnd \land w \in Word B) \to \sum_{M} w \in B$
43	36 40 42	syl2anc	$⊢ ((φ \land g \in F) \land w \in Word A) \to \sum_{M} w \in B$
44	1 3 26 33 43	mulgcld	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
45	44	fmpttd	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) : Word A ⟶ B$
46	32	feqmptd	$⊢ (φ \land g \in F) \to g = (w \in Word A ⟼ g (w))$
47	29	simprd	$⊢ g \in F \to {finSupp}_{0} (g)$
48	47	adantl	$⊢ (φ \land g \in F) \to {finSupp}_{0} (g)$
49	46 48	eqbrtrrd	$⊢ (φ \land g \in F) \to {finSupp}_{0} ((w \in Word A ⟼ g (w)))$
50	1 16 3	mulg0	$⊢ y \in B \to 0 \underset{˙}{\cdot} y = 0_{R}$
51	50	adantl	$⊢ ((φ \land g \in F) \land y \in B) \to 0 \underset{˙}{\cdot} y = 0_{R}$
52		fvexd	$⊢ (φ \land g \in F) \to 0_{R} \in V$
53	49 51 33 43 52	fsuppssov1	$⊢ (φ \land g \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
54	1 16 18 24 45 53	gsumcl	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in B$
55	54	adantr	$⊢ ((φ \land g \in F) \land X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in B$
56	15 55	eqeltrd	$⊢ ((φ \land g \in F) \land X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to X \in B$
57	56	r19.29an	$⊢ (φ \land \exists g \in F X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to X \in B$
58	6	adantr	$⊢ (φ \land X \in B) \to R \in Ring$
59	7	adantr	$⊢ (φ \land X \in B) \to A \subseteq B$
60		fveq1	$⊢ h = i \to h (w) = i (w)$
61	60	oveq1d	$⊢ h = i \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (w) \underset{˙}{\cdot} (\sum_{M}, w)$
62	61	mpteq2dv	$⊢ h = i \to (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
63		fveq2	$⊢ w = v \to i (w) = i (v)$
64		oveq2	$⊢ w = v \to \sum_{M} w = \sum_{M} v$
65	63 64	oveq12d	$⊢ w = v \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (v) \underset{˙}{\cdot} (\sum_{M}, v)$
66	65	cbvmptv	$⊢ (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (v \in Word A ⟼ i (v) \underset{˙}{\cdot} (\sum_{M}, v))$
67	62 66	eqtrdi	$⊢ h = i \to (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (v \in Word A ⟼ i (v) \underset{˙}{\cdot} (\sum_{M}, v))$
68	67	oveq2d	$⊢ h = i \to \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{v \in Word A}{\sum_{R}} (i (v) \underset{˙}{\cdot} (\sum_{M}, v))$
69	68	cbvmptv	$⊢ (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (i \in F ⟼ \underset{v \in Word A}{\sum_{R}} (i (v) \underset{˙}{\cdot} (\sum_{M}, v)))$
70	69	rneqi	$⊢ ran (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))) = ran (i \in F ⟼ \underset{v \in Word A}{\sum_{R}} (i (v) \underset{˙}{\cdot} (\sum_{M}, v)))$
71	1 2 3 4 5 58 59 70	elrgspnlem4	$⊢ (φ \land X \in B) \to N (A) = ran (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
72	71	eleq2d	$⊢ (φ \land X \in B) \to (X \in N (A) \leftrightarrow X \in ran (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))))$
73		fveq1	$⊢ h = g \to h (w) = g (w)$
74	73	oveq1d	$⊢ h = g \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = g (w) \underset{˙}{\cdot} (\sum_{M}, w)$
75	74	mpteq2dv	$⊢ h = g \to (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
76	75	oveq2d	$⊢ h = g \to \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
77	76	cbvmptv	$⊢ (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
78	77	elrnmpt	$⊢ X \in B \to (X \in ran (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \exists g \in F X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
79	78	adantl	$⊢ (φ \land X \in B) \to (X \in ran (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \exists g \in F X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
80	72 79	bitrd	$⊢ (φ \land X \in B) \to (X \in N (A) \leftrightarrow \exists g \in F X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
81	14 57 80	bibiad	$⊢ φ \to (X \in N (A) \leftrightarrow \exists g \in F X = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$

Metamath Proof Explorer

Theorem elrgspn

Proof