Theorem elrsp

Description: Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	elrsp.n	$$⊢N=\mathrm{RSpan}\left(R\right)$$
	elrsp.b	$$⊢B={\mathrm{Base}}_R$$
	elrsp.1	$$⊢\underset{\dot{}}{0}=0_R$$
	elrsp.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	elrsp.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	elrsp.i	$$⊢\phi \to I\subseteq B$$
Assertion	elrsp	$$⊢\phi \to \left(X\in N\left(I\right)\leftrightarrow \exists a\in \left(B^I\right)\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_R}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrsp.n	$$⊢N=\mathrm{RSpan}\left(R\right)$$
2		elrsp.b	$$⊢B={\mathrm{Base}}_R$$
3		elrsp.1	$$⊢\underset{\dot{}}{0}=0_R$$
4		elrsp.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		elrsp.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		elrsp.i	$$⊢\phi \to I\subseteq B$$
7		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
8	1 7	eqtri	$$⊢N=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
9		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
10	2 9	eqtri	$$⊢B={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
12		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
13		eqid	$$⊢0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}=0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
14		rlmvsca	$$⊢{\cdot }_R={\cdot }_{\mathrm{ringLMod}\left(R\right)}$$
15	4 14	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{ringLMod}\left(R\right)}$$
16		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
17	5 16	syl	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
18	8 10 11 12 13 15 17 6	ellspds	$$⊢\phi \to \left(X\in N\left(I\right)\leftrightarrow \exists a\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}^I\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_{\mathrm{ringLMod}\left(R\right)}}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\right)$$
19		rlmsca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
20	5 19	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
21	20	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
22	2 21	syl5eq	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
23	22	oveq1d	$$⊢\phi \to B^I={{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}^I$$
24	20	fveq2d	$$⊢\phi \to 0_R=0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
25	3 24	syl5eq	$$⊢\phi \to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
26	25	breq2d	$$⊢\phi \to \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\leftrightarrow {finSupp}_{0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}\left(a\right)\right)$$
27	2	fvexi	$$⊢B\in \mathrm{V}$$
28	27	a1i	$$⊢\phi \to B\in \mathrm{V}$$
29	28 6	ssexd	$$⊢\phi \to I\in \mathrm{V}$$
30	29	mptexd	$$⊢\phi \to \left(i\in I⟼a\left(i\right)\underset{\dot{}}{·}i\right)\in \mathrm{V}$$
31	9	a1i	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
32		rlmplusg	$$⊢{+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
33	32	a1i	$$⊢\phi \to {+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
34	30 5 17 31 33	gsumpropd	$$⊢\phi \to \underset{i\in I}{{\sum }_R}\left(a\left(i\right)\underset{\dot{}}{·}i\right)=\underset{i\in I}{{\sum }_{\mathrm{ringLMod}\left(R\right)}}\left(a\left(i\right)\underset{\dot{}}{·}i\right)$$
35	34	eqeq2d	$$⊢\phi \to \left(X=\underset{i\in I}{{\sum }_R}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\leftrightarrow X=\underset{i\in I}{{\sum }_{\mathrm{ringLMod}\left(R\right)}}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)$$
36	26 35	anbi12d	$$⊢\phi \to \left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_R}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\leftrightarrow \left({finSupp}_{0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_{\mathrm{ringLMod}\left(R\right)}}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\right)$$
37	23 36	rexeqbidv	$$⊢\phi \to \left(\exists a\in \left(B^I\right)\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_R}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\leftrightarrow \exists a\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}^I\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_{\mathrm{ringLMod}\left(R\right)}}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\right)$$
38	18 37	bitr4d	$$⊢\phi \to \left(X\in N\left(I\right)\leftrightarrow \exists a\in \left(B^I\right)\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge X=\underset{i\in I}{{\sum }_R}\left(a\left(i\right)\underset{\dot{}}{·}i\right)\right)\right)$$