Definition df-lininds

Description: Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019) (Revised by AV, 24-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Assertion	df-lininds	$$⊢\mathrm{linIndS}=\left\{⟨s,m⟩|\left(s\in 𝒫{\mathrm{Base}}_m\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clininds	$$class\mathrm{linIndS}$$
1		vs	$$setvars$$
2		vm	$$setvarm$$
3	1	cv	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	2	cv	$$setvarm$$
6	5 4	cfv	$$class{\mathrm{Base}}_m$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_m$$
8	3 7	wcel	$$wffs\in 𝒫{\mathrm{Base}}_m$$
9		vf	$$setvarf$$
10		csca	$$class\mathrm{Scalar}$$
11	5 10	cfv	$$class\mathrm{Scalar}\left(m\right)$$
12	11 4	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}$$
13		cmap	$$class{\uparrow }_{𝑚}$$
14	12 3 13	co	$$class\left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)$$
15	9	cv	$$setvarf$$
16		cfsupp	$$class\mathrm{finSupp}$$
17		c0g	$$class{0}_{𝑔}$$
18	11 17	cfv	$$class{0}_{\mathrm{Scalar}\left(m\right)}$$
19	15 18 16	wbr	$$wff{finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)$$
20		clinc	$$class\mathrm{linC}$$
21	5 20	cfv	$$class\mathrm{linC}\left(m\right)$$
22	15 3 21	co	$$class\left(f\mathrm{linC}\left(m\right)s\right)$$
23	5 17	cfv	$$class{0}_m$$
24	22 23	wceq	$$wfff\mathrm{linC}\left(m\right)s=0_m$$
25	19 24	wa	$$wff\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)$$
26		vx	$$setvarx$$
27	26	cv	$$setvarx$$
28	27 15	cfv	$$classf\left(x\right)$$
29	28 18	wceq	$$wfff\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}$$
30	29 26 3	wral	$$wff\forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}$$
31	25 30	wi	$$wff\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)$$
32	31 9 14	wral	$$wff\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)$$
33	8 32	wa	$$wff\left(s\in 𝒫{\mathrm{Base}}_m\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)\right)$$
34	33 1 2	copab	$$class\left\{⟨s,m⟩|\left(s\in 𝒫{\mathrm{Base}}_m\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)\right)\right\}$$
35	0 34	wceq	$$wff\mathrm{linIndS}=\left\{⟨s,m⟩|\left(s\in 𝒫{\mathrm{Base}}_m\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)\right)\right\}$$