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	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
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	1	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
9	4	a1i	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
10		eqidd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) = ( 𝑁 ‘ 𝐴 ) )
11	6 8 7 9 10	rgspncl	⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ∈ ( SubRing ‘ 𝑅 ) )
12	1	subrgss	⊢ ( ( 𝑁 ‘ 𝐴 ) ∈ ( SubRing ‘ 𝑅 ) → ( 𝑁 ‘ 𝐴 ) ⊆ 𝐵 )
13	11 12	syl	⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ⊆ 𝐵 )
14	13	sselda	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
15		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
16		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17	6	ringcmnd	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑅 ∈ CMnd )
19	1	fvexi	⊢ 𝐵 ∈ V
20	19	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
21	20 7	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝐴 ∈ V )
23		wrdexg	⊢ ( 𝐴 ∈ V → Word 𝐴 ∈ V )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → Word 𝐴 ∈ V )
25	6	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑅 ∈ Grp )
27		breq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 finSupp 0 ↔ 𝑔 finSupp 0 ) )
28	27 5	elrab2	⊢ ( 𝑔 ∈ 𝐹 ↔ ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
29	28	biimpi	⊢ ( 𝑔 ∈ 𝐹 → ( 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) ∧ 𝑔 finSupp 0 ) )
30	29	simpld	⊢ ( 𝑔 ∈ 𝐹 → 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑔 ∈ ( ℤ ↑m Word 𝐴 ) )
32	31	elmaprd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑔 : Word 𝐴 ⟶ ℤ )
33	32	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑔 ‘ 𝑤 ) ∈ ℤ )
34	2	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
35	6 34	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
36	35	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑀 ∈ Mnd )
37		sswrd	⊢ ( 𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵 )
38	7 37	syl	⊢ ( 𝜑 → Word 𝐴 ⊆ Word 𝐵 )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → Word 𝐴 ⊆ Word 𝐵 )
40	39	sselda	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → 𝑤 ∈ Word 𝐵 )
41	2 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
42	41	gsumwcl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
43	36 40 42	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑀 Σg 𝑤 ) ∈ 𝐵 )
44	1 3 26 33 43	mulgcld	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ∈ 𝐵 )
45	44	fmpttd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) : Word 𝐴 ⟶ 𝐵 )
46	32	feqmptd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑔 = ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑔 ‘ 𝑤 ) ) )
47	29	simprd	⊢ ( 𝑔 ∈ 𝐹 → 𝑔 finSupp 0 )
48	47	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑔 finSupp 0 )
49	46 48	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑔 ‘ 𝑤 ) ) finSupp 0 )
50	1 16 3	mulg0	⊢ ( 𝑦 ∈ 𝐵 → ( 0 · 𝑦 ) = ( 0g ‘ 𝑅 ) )
51	50	adantl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝐵 ) → ( 0 · 𝑦 ) = ( 0g ‘ 𝑅 ) )
52		fvexd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 0g ‘ 𝑅 ) ∈ V )
53	49 51 33 43 52	fsuppssov1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
54	1 16 18 24 45 53	gsumcl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
55	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ∈ 𝐵 )
56	15 55	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑋 ∈ 𝐵 )
57	56	r19.29an	⊢ ( ( 𝜑 ∧ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) → 𝑋 ∈ 𝐵 )
58	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
59	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 )
60		fveq1	⊢ ( ℎ = 𝑖 → ( ℎ ‘ 𝑤 ) = ( 𝑖 ‘ 𝑤 ) )
61	60	oveq1d	⊢ ( ℎ = 𝑖 → ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
62	61	mpteq2dv	⊢ ( ℎ = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
63		fveq2	⊢ ( 𝑤 = 𝑣 → ( 𝑖 ‘ 𝑤 ) = ( 𝑖 ‘ 𝑣 ) )
64		oveq2	⊢ ( 𝑤 = 𝑣 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 𝑣 ) )
65	63 64	oveq12d	⊢ ( 𝑤 = 𝑣 → ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) )
66	65	cbvmptv	⊢ ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) )
67	62 66	eqtrdi	⊢ ( ℎ = 𝑖 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) )
68	67	oveq2d	⊢ ( ℎ = 𝑖 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
69	68	cbvmptv	⊢ ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑖 ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
70	69	rneqi	⊢ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ran ( 𝑖 ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑣 ∈ Word 𝐴 ↦ ( ( 𝑖 ‘ 𝑣 ) · ( 𝑀 Σg 𝑣 ) ) ) ) )
71	1 2 3 4 5 58 59 70	elrgspnlem4	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝐴 ) = ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
72	71	eleq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ↔ 𝑋 ∈ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ) )
73		fveq1	⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑤 ) = ( 𝑔 ‘ 𝑤 ) )
74	73	oveq1d	⊢ ( ℎ = 𝑔 → ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) = ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) )
75	74	mpteq2dv	⊢ ( ℎ = 𝑔 → ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) )
76	75	oveq2d	⊢ ( ℎ = 𝑔 → ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
77	76	cbvmptv	⊢ ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) = ( 𝑔 ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) )
78	77	elrnmpt	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
79	78	adantl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ran ( ℎ ∈ 𝐹 ↦ ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( ℎ ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
80	72 79	bitrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )
81	14 57 80	bibiad	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ 𝐴 ) ↔ ∃ 𝑔 ∈ 𝐹 𝑋 = ( 𝑅 Σg ( 𝑤 ∈ Word 𝐴 ↦ ( ( 𝑔 ‘ 𝑤 ) · ( 𝑀 Σg 𝑤 ) ) ) ) ) )