Theorem islbs5

Description: An equivalent formulation of the basis predicate in a vector space, using a function F for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	islbs5.b	$$⊢B={\mathrm{Base}}_W$$
	islbs5.k	$$⊢K={\mathrm{Base}}_S$$
	islbs5.r	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	islbs5.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	islbs5.z	$$⊢O=0_W$$
	islbs5.y	$$⊢\underset{\dot{}}{0}=0_S$$
	islbs5.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
	islbs5.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	islbs5.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	islbs5.s	$$⊢\phi \to S\in \mathrm{NzRing}$$
	islbs5.i	$$⊢\phi \to I\in V$$
	islbs5.f	$$⊢\phi \to F:I\underset{1-1}{⟶}B$$
Assertion	islbs5	$$⊢\phi \to \left(\mathrm{ran}F\in \mathrm{LBasis}\left(W\right)\leftrightarrow \left(\forall a\in \left(K^I\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\wedge N\left(\mathrm{ran}F\right)=B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islbs5.b	$$⊢B={\mathrm{Base}}_W$$
2		islbs5.k	$$⊢K={\mathrm{Base}}_S$$
3		islbs5.r	$$⊢S=\mathrm{Scalar}\left(W\right)$$
4		islbs5.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		islbs5.z	$$⊢O=0_W$$
6		islbs5.y	$$⊢\underset{\dot{}}{0}=0_S$$
7		islbs5.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
8		islbs5.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
9		islbs5.w	$$⊢\phi \to W\in \mathrm{LMod}$$
10		islbs5.s	$$⊢\phi \to S\in \mathrm{NzRing}$$
11		islbs5.i	$$⊢\phi \to I\in V$$
12		islbs5.f	$$⊢\phi \to F:I\underset{1-1}{⟶}B$$
13		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
14	1 13 3 4 5 6 8 9 10 11 12	lindflbs	$$⊢\phi \to \left(\mathrm{ran}F\in \mathrm{LBasis}\left(W\right)\leftrightarrow \left(F\mathrm{LIndF}W\wedge N\left(\mathrm{ran}F\right)=B\right)\right)$$
15		f1f	$$⊢F:I\underset{1-1}{⟶}B\to F:I⟶B$$
16	12 15	syl	$$⊢\phi \to F:I⟶B$$
17		eqid	$$⊢{\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}$$
18	1 3 4 5 6 17	islindf4	$$⊢\left(W\in \mathrm{LMod}\wedge I\in V\wedge F:I⟶B\right)\to \left(F\mathrm{LIndF}W\leftrightarrow \forall a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
19	9 11 16 18	syl3anc	$$⊢\phi \to \left(F\mathrm{LIndF}W\leftrightarrow \forall a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
20	10	elexd	$$⊢\phi \to S\in \mathrm{V}$$
21		eqid	$$⊢S\mathrm{freeLMod}I=S\mathrm{freeLMod}I$$
22	21 2 6 17	frlmelbas	$$⊢\left(S\in \mathrm{V}\wedge I\in V\right)\to \left(a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\leftrightarrow \left(a\in \left(K^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right)\right)$$
23	20 11 22	syl2anc	$$⊢\phi \to \left(a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\leftrightarrow \left(a\in \left(K^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right)\right)$$
24	23	imbi1d	$$⊢\phi \to \left(\left(a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(\left(a\in \left(K^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
25		impexp	$$⊢\left(\left(a\in \left(K^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(a\in \left(K^I\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
26		impexp	$$⊢\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
27	26	a1i	$$⊢\phi \to \left(\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
28	27	bicomd	$$⊢\phi \to \left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
29	28	imbi2d	$$⊢\phi \to \left(\left(a\in \left(K^I\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\leftrightarrow \left(a\in \left(K^I\right)\to \left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
30	25 29	bitrid	$$⊢\phi \to \left(\left(\left(a\in \left(K^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(a\right)\right)\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(a\in \left(K^I\right)\to \left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
31	24 30	bitrd	$$⊢\phi \to \left(\left(a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\to \left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\leftrightarrow \left(a\in \left(K^I\right)\to \left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
32	31	ralbidv2	$$⊢\phi \to \left(\forall a\in {\mathrm{Base}}_{\left(S\mathrm{freeLMod}I\right)}\left({\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \forall a\in \left(K^I\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
33	19 32	bitrd	$$⊢\phi \to \left(F\mathrm{LIndF}W\leftrightarrow \forall a\in \left(K^I\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
34	33	anbi1d	$$⊢\phi \to \left(\left(F\mathrm{LIndF}W\wedge N\left(\mathrm{ran}F\right)=B\right)\leftrightarrow \left(\forall a\in \left(K^I\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\wedge N\left(\mathrm{ran}F\right)=B\right)\right)$$
35	14 34	bitrd	$$⊢\phi \to \left(\mathrm{ran}F\in \mathrm{LBasis}\left(W\right)\leftrightarrow \left(\forall a\in \left(K^I\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(a\right)\wedge {\sum }_W\left(a{\underset{\dot{}}{·}}_{f}F\right)=O\right)\to a=I\times \left\{\underset{\dot{}}{0}\right\}\right)\wedge N\left(\mathrm{ran}F\right)=B\right)\right)$$