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		zex	$⊢ ℤ \in V$
28	27	a1i	$⊢ (φ \land g \in F) \to ℤ \in V$
29		breq1	$⊢ f = g \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (g))$
30	29 5	elrab2	$⊢ g \in F \leftrightarrow (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
31	30	biimpi	$⊢ g \in F \to (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
32	31	simpld	$⊢ g \in F \to g \in (ℤ^{Word A})$
33	32	adantl	$⊢ (φ \land g \in F) \to g \in (ℤ^{Word A})$
34	24 28 33	elmaprd	$⊢ (φ \land g \in F) \to g : Word A ⟶ ℤ$
35	34	ffvelcdmda	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \in ℤ$
36	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
37	6 36	syl	$⊢ φ \to M \in Mnd$
38	37	ad2antrr	$⊢ ((φ \land g \in F) \land w \in Word A) \to M \in Mnd$
39		sswrd	$⊢ A \subseteq B \to Word A \subseteq Word B$
40	7 39	syl	$⊢ φ \to Word A \subseteq Word B$
41	40	adantr	$⊢ (φ \land g \in F) \to Word A \subseteq Word B$
42	41	sselda	$⊢ ((φ \land g \in F) \land w \in Word A) \to w \in Word B$
43	2 1	mgpbas	$⊢ B = {Base}_{M}$
44	43	gsumwcl	$⊢ (M \in Mnd \land w \in Word B) \to \sum_{M} w \in B$
45	38 42 44	syl2anc	$⊢ ((φ \land g \in F) \land w \in Word A) \to \sum_{M} w \in B$
46	1 3 26 35 45	mulgcld	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
47	46	fmpttd	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) : Word A ⟶ B$
48	34	feqmptd	$⊢ (φ \land g \in F) \to g = (w \in Word A ⟼ g (w))$
49	31	simprd	$⊢ g \in F \to {finSupp}_{0} (g)$
50	49	adantl	$⊢ (φ \land g \in F) \to {finSupp}_{0} (g)$
51	48 50	eqbrtrrd	$⊢ (φ \land g \in F) \to {finSupp}_{0} ((w \in Word A ⟼ g (w)))$
52	1 16 3	mulg0	$⊢ y \in B \to 0 \underset{˙}{\cdot} y = 0_{R}$
53	52	adantl	$⊢ ((φ \land g \in F) \land y \in B) \to 0 \underset{˙}{\cdot} y = 0_{R}$
54		fvexd	$⊢ (φ \land g \in F) \to 0_{R} \in V$
55	51 53 35 45 54	fsuppssov1	$⊢ (φ \land g \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
56	1 16 18 24 47 55	gsumcl	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in B$
57	56	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$
58	15 57	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$
59	58	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$
60	6	adantr	$⊢ (φ \land X \in B) \to R \in Ring$
61	7	adantr	$⊢ (φ \land X \in B) \to A \subseteq B$
62		fveq1	$⊢ h = i \to h (w) = i (w)$
63	62	oveq1d	$⊢ h = i \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (w) \underset{˙}{\cdot} (\sum_{M}, w)$
64	63	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))$
65		fveq2	$⊢ w = v \to i (w) = i (v)$
66		oveq2	$⊢ w = v \to \sum_{M} w = \sum_{M} v$
67	65 66	oveq12d	$⊢ w = v \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (v) \underset{˙}{\cdot} (\sum_{M}, v)$
68	67	cbvmptv	$⊢ (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (v \in Word A ⟼ i (v) \underset{˙}{\cdot} (\sum_{M}, v))$
69	64 68	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))$
70	69	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))$
71	70	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)))$
72	71	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)))$
73	1 2 3 4 5 60 61 72	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)))$
74	73	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))))$
75		fveq1	$⊢ h = g \to h (w) = g (w)$
76	75	oveq1d	$⊢ h = g \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = g (w) \underset{˙}{\cdot} (\sum_{M}, w)$
77	76	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))$
78	77	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))$
79	78	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)))$
80	79	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)))$
81	80	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)))$
82	74 81	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)))$
83	14 59 82	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