Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elrgspn.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	elrgspn.x	⊢ · = ( .g ‘ 𝑅 )
	elrgspn.n	⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
	elrgspn.f	⊢ 𝐹 = { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 }
	elrgspn.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	elrgspn.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	elrgspn.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	elrgspn	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrgspn.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elrgspn.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3		elrgspn.x	⊢ · = ( .g ‘ 𝑅 )
4		elrgspn.n	⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
5		elrgspn.f	⊢ 𝐹 = { 𝑓 ∈ ( ℤ ↑m Word 𝐴 ) ∣ 𝑓 finSupp 0 }
6		elrgspn.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		elrgspn.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
8		elrgspn.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		fveq1	⊢ ( ℎ = 𝑖 → ( ℎ ‘ 𝑤 ) = ( 𝑖 ‘ 𝑤 ) )
10	9	oveq1d	⊢ ( ℎ = 𝑖 → ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
11	10	mpteq2dv	⊢ ( ℎ = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
12		fveq2	⊢ ( 𝑤 = 𝑣 → ( 𝑖 ‘ 𝑤 ) = ( 𝑖 ‘ 𝑣 ) )
13		oveq2	⊢ ( 𝑤 = 𝑣 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 𝑣 ) )
14	12 13	oveq12d	⊢ ( 𝑤 = 𝑣 → ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) )
15	14	cbvmptv	⊢ ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) )
16	11 15	eqtrdi	⊢ ( ℎ = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) )
17	16	oveq2d	⊢ ( ℎ = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
18	17	cbvmptv	⊢ ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑖 ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
19	18	rneqi	⊢ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ran ( 𝑖 ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
20	1 2 3 4 5 6 7 19	elrgspnlem4	⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) = ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
21	20	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ↔ 𝑋 ∈ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ) )
22		fveq1	⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑤 ) = ( 𝑔 ‘ 𝑤 ) )
23	22	oveq1d	⊢ ( ℎ = 𝑔 → ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
24	23	mpteq2dv	⊢ ( ℎ = 𝑔 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
25	24	oveq2d	⊢ ( ℎ = 𝑔 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
26	25	cbvmptv	⊢ ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔 ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
27	26	elrnmpt	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
28	8 27	syl	⊢ ( 𝜑 → ( 𝑋 ∈ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
29	21 28	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )