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$
	elrgspn.1	$⊢ φ \to X \in 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		elrgspn.1	$⊢ φ \to X \in B$
9		fveq1	$⊢ h = i \to h (w) = i (w)$
10	9	oveq1d	$⊢ h = i \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (w) \underset{˙}{\cdot} (\sum_{M}, w)$
11	10	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))$
12		fveq2	$⊢ w = v \to i (w) = i (v)$
13		oveq2	$⊢ w = v \to \sum_{M} w = \sum_{M} v$
14	12 13	oveq12d	$⊢ w = v \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (v) \underset{˙}{\cdot} (\sum_{M}, v)$
15	14	cbvmptv	$⊢ (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (v \in Word A ⟼ i (v) \underset{˙}{\cdot} (\sum_{M}, v))$
16	11 15	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))$
17	16	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))$
18	17	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)))$
19	18	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)))$
20	1 2 3 4 5 6 7 19	elrgspnlem4	$⊢ φ \to N (A) = ran (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
21	20	eleq2d	$⊢ φ \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))))$
22		fveq1	$⊢ h = g \to h (w) = g (w)$
23	22	oveq1d	$⊢ h = g \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = g (w) \underset{˙}{\cdot} (\sum_{M}, w)$
24	23	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))$
25	24	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))$
26	25	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)))$
27	26	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)))$
28	8 27	syl	$⊢ φ \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)))$
29	21 28	bitrd	$⊢ φ \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