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