Theorem ldepsnlinc

Description: The reverse implication of islindeps2 does not hold for arbitrary (left) modules, see note in Roman p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa and zlmodzxznm . (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Assertion	ldepsnlinc	$$⊢\exists m\in \mathrm{LMod}\exists s\in 𝒫{\mathrm{Base}}_m\left(s\mathrm{linDepS}m\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2	1	zlmodzxzlmod	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\right)$$
3	2	simpli	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{LMod}$$
4		3z	$$⊢3\in \mathbb{Z}$$
5		6nn	$$⊢6\in \mathbb{N}$$
6	5	nnzi	$$⊢6\in \mathbb{Z}$$
7	1	zlmodzxzel	$$⊢\left(3\in \mathbb{Z}\wedge 6\in \mathbb{Z}\right)\to \left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
8	4 6 7	mp2an	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
9		2z	$$⊢2\in \mathbb{Z}$$
10		4z	$$⊢4\in \mathbb{Z}$$
11	1	zlmodzxzel	$$⊢\left(2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
12	9 10 11	mp2an	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
13		prelpwi	$$⊢\left(\left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\wedge \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\right)\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
14	8 12 13	mp2an	$$⊢\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
15		eqid	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
16		eqid	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
17	1 15 16	zlmodzxzldep	$$⊢\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)$$
18	1 15 16	ldepsnlinclem1	$$⊢f\in \left({{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}$$
19		simpr	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\right)\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)$$
20	19	eqcomd	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\right)\to \mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)={\mathbb{Z}}_{\mathrm{ring}}$$
21	2 20	ax-mp	$$⊢\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)={\mathbb{Z}}_{\mathrm{ring}}$$
22	21	fveq2i	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
23	22	oveq1i	$$⊢{{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}={{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}$$
24	18 23	eleq2s	$$⊢f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}$$
25	24	a1d	$$⊢f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}\right)\to \left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}\right)$$
26	25	rgen	$$⊢\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}\right)$$
27	1 15 16	ldepsnlinclem2	$$⊢f\in \left({{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}$$
28	22	oveq1i	$$⊢{{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}={{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}$$
29	27 28	eleq2s	$$⊢f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}$$
30	29	a1d	$$⊢f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}\right)\to \left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)$$
31	30	rgen	$$⊢\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)$$
32		prex	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\in \mathrm{V}$$
33		prex	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in \mathrm{V}$$
34		sneq	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to \left\{v\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}$$
35	34	difeq2d	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}$$
36	1 15 16	zlmodzxzldeplem	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}$$
37		difprsn1	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}=\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
38	36 37	ax-mp	$$⊢\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}=\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
39	35 38	eqtrdi	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}=\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
40	39	oveq2d	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}={{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}$$
41	39	oveq2d	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)=f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
42		id	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to v=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
43	41 42	neeq12d	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to \left(f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\leftrightarrow f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}\right)$$
44	43	imbi2d	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to \left(\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}\right)\right)$$
45	40 44	raleqbidv	$$⊢v=\left\{⟨0,3⟩,⟨1,6⟩\right\}\to \left(\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}\right)\right)$$
46		sneq	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left\{v\right\}=\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
47	46	difeq2d	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
48		difprsn2	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}$$
49	36 48	ax-mp	$$⊢\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}$$
50	47 49	eqtrdi	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}$$
51	50	oveq2d	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}={{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}$$
52	50	oveq2d	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)=f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}$$
53		id	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to v=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
54	52 53	neeq12d	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left(f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\leftrightarrow f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)$$
55	54	imbi2d	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left(\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)\right)$$
56	51 55	raleqbidv	$$⊢v=\left\{⟨0,2⟩,⟨1,4⟩\right\}\to \left(\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)\right)$$
57	32 33 45 56	ralpr	$$⊢\forall v\in \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \left(\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\ne \left\{⟨0,3⟩,⟨1,6⟩\right\}\right)\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\}\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)\right)$$
58	26 31 57	mpbir2an	$$⊢\forall v\in \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)$$
59	17 58	pm3.2i	$$⊢\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\right)$$
60		breq1	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to \left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\leftrightarrow \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\right)$$
61		id	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}$$
62		difeq1	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to s\setminus \left\{v\right\}=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}$$
63	62	oveq2d	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}={{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}$$
64	62	oveq2d	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)=f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)$$
65	64	neeq1d	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to \left(f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\leftrightarrow f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)$$
66	65	imbi2d	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to \left(\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\right)$$
67	63 66	raleqbidv	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to \left(\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\right)$$
68	61 67	raleqbidv	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to \left(\forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \forall v\in \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\right)$$
69	60 68	anbi12d	$$⊢s=\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\to \left(\left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)\leftrightarrow \left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\right)\right)$$
70	69	rspcev	$$⊢\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\wedge \left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in \left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(\left\{\left\{⟨0,3⟩,⟨1,6⟩\right\},\left\{⟨0,2⟩,⟨1,4⟩\right\}\right\}\setminus \left\{v\right\}\right)\ne v\right)\right)\right)\to \exists s\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$
71	14 59 70	mp2an	$$⊢\exists s\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$
72		fveq2	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to {\mathrm{Base}}_m={\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
73	72	pweqd	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to 𝒫{\mathrm{Base}}_m=𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
74		breq2	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(s\mathrm{linDepS}m\leftrightarrow s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\right)$$
75		2fveq3	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
76	75	oveq1d	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}={{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}$$
77		2fveq3	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to 0_{\mathrm{Scalar}\left(m\right)}=0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}$$
78	77	breq2d	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\leftrightarrow {finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\right)$$
79		fveq2	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \mathrm{linC}\left(m\right)=\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)$$
80	79	oveqd	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)=f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)$$
81	80	neeq1d	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\leftrightarrow f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)$$
82	78 81	imbi12d	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$
83	76 82	raleqbidv	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$
84	83	ralbidv	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(\forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\leftrightarrow \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$
85	74 84	anbi12d	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(\left(s\mathrm{linDepS}m\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)\leftrightarrow \left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)\right)$$
86	73 85	rexeqbidv	$$⊢m={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\to \left(\exists s\in 𝒫{\mathrm{Base}}_m\left(s\mathrm{linDepS}m\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)\leftrightarrow \exists s\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)\right)$$
87	86	rspcev	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{LMod}\wedge \exists s\in 𝒫{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}\left(s\mathrm{linDepS}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)}}\left(f\right)\to f\mathrm{linC}\left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)\right)\to \exists m\in \mathrm{LMod}\exists s\in 𝒫{\mathrm{Base}}_m\left(s\mathrm{linDepS}m\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$
88	3 71 87	mp2an	$$⊢\exists m\in \mathrm{LMod}\exists s\in 𝒫{\mathrm{Base}}_m\left(s\mathrm{linDepS}m\wedge \forall v\in s\forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^{\left(s\setminus \left\{v\right\}\right)}\right)\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\to f\mathrm{linC}\left(m\right)\left(s\setminus \left\{v\right\}\right)\ne v\right)\right)$$