Theorem zlmodzxzldep

Description: { A , B } is a linearly dependent set within the ZZ-module ZZ X. ZZ (see example in Roman p. 112). (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxzldep.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
	zlmodzxzldep.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
	zlmodzxzldep.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
Assertion	zlmodzxzldep	$$⊢\left\{A,B\right\}\mathrm{linDepS}Z$$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2		zlmodzxzldep.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
3		zlmodzxzldep.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
4		eqid	$$⊢\left\{⟨A,2⟩,⟨B,-3⟩\right\}=\left\{⟨A,2⟩,⟨B,-3⟩\right\}$$
5	1 2 3 4	zlmodzxzldeplem1	$$⊢\left\{⟨A,2⟩,⟨B,-3⟩\right\}\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)$$
6	1 2 3 4	zlmodzxzldeplem2	$$⊢{finSupp}_0\left(\left\{⟨A,2⟩,⟨B,-3⟩\right\}\right)$$
7	1 2 3 4	zlmodzxzldeplem3	$$⊢\left\{⟨A,2⟩,⟨B,-3⟩\right\}\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z$$
8	1 2 3 4	zlmodzxzldeplem4	$$⊢\exists y\in \left\{A,B\right\}\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)\ne 0$$
9	6 7 8	3pm3.2i	$$⊢\left({finSupp}_0\left(\left\{⟨A,2⟩,⟨B,-3⟩\right\}\right)\wedge \left\{⟨A,2⟩,⟨B,-3⟩\right\}\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)\ne 0\right)$$
10		breq1	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to \left({finSupp}_0\left(x\right)\leftrightarrow {finSupp}_0\left(\left\{⟨A,2⟩,⟨B,-3⟩\right\}\right)\right)$$
11		oveq1	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\mathrm{linC}\left(Z\right)\left\{A,B\right\}$$
12	11	eqeq1d	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to \left(x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\leftrightarrow \left\{⟨A,2⟩,⟨B,-3⟩\right\}\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\right)$$
13		fveq1	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to x\left(y\right)=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)$$
14	13	neeq1d	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to \left(x\left(y\right)\ne 0\leftrightarrow \left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)\ne 0\right)$$
15	14	rexbidv	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to \left(\exists y\in \left\{A,B\right\}x\left(y\right)\ne 0\leftrightarrow \exists y\in \left\{A,B\right\}\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)\ne 0\right)$$
16	10 12 15	3anbi123d	$$⊢x=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\to \left(\left({finSupp}_0\left(x\right)\wedge x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}x\left(y\right)\ne 0\right)\leftrightarrow \left({finSupp}_0\left(\left\{⟨A,2⟩,⟨B,-3⟩\right\}\right)\wedge \left\{⟨A,2⟩,⟨B,-3⟩\right\}\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)\ne 0\right)\right)$$
17	16	rspcev	$$⊢\left(\left\{⟨A,2⟩,⟨B,-3⟩\right\}\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)\wedge \left({finSupp}_0\left(\left\{⟨A,2⟩,⟨B,-3⟩\right\}\right)\wedge \left\{⟨A,2⟩,⟨B,-3⟩\right\}\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(y\right)\ne 0\right)\right)\to \exists x\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)\left({finSupp}_0\left(x\right)\wedge x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}x\left(y\right)\ne 0\right)$$
18	5 9 17	mp2an	$$⊢\exists x\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)\left({finSupp}_0\left(x\right)\wedge x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}x\left(y\right)\ne 0\right)$$
19		ovex	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{V}$$
20	1 19	eqeltri	$$⊢Z\in \mathrm{V}$$
21		3z	$$⊢3\in \mathbb{Z}$$
22		6nn	$$⊢6\in \mathbb{N}$$
23	22	nnzi	$$⊢6\in \mathbb{Z}$$
24	1	zlmodzxzel	$$⊢\left(3\in \mathbb{Z}\wedge 6\in \mathbb{Z}\right)\to \left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_Z$$
25	21 23 24	mp2an	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_Z$$
26	2 25	eqeltri	$$⊢A\in {\mathrm{Base}}_Z$$
27		2z	$$⊢2\in \mathbb{Z}$$
28		4z	$$⊢4\in \mathbb{Z}$$
29	1	zlmodzxzel	$$⊢\left(2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
30	27 28 29	mp2an	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
31	3 30	eqeltri	$$⊢B\in {\mathrm{Base}}_Z$$
32		prelpwi	$$⊢\left(A\in {\mathrm{Base}}_Z\wedge B\in {\mathrm{Base}}_Z\right)\to \left\{A,B\right\}\in 𝒫{\mathrm{Base}}_Z$$
33	26 31 32	mp2an	$$⊢\left\{A,B\right\}\in 𝒫{\mathrm{Base}}_Z$$
34		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
35		eqid	$$⊢0_Z=0_Z$$
36	1	zlmodzxzlmod	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)$$
37	36	simpri	$$⊢{\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)$$
38		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
39		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
40	34 35 37 38 39	islindeps	$$⊢\left(Z\in \mathrm{V}\wedge \left\{A,B\right\}\in 𝒫{\mathrm{Base}}_Z\right)\to \left(\left\{A,B\right\}\mathrm{linDepS}Z\leftrightarrow \exists x\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)\left({finSupp}_0\left(x\right)\wedge x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}x\left(y\right)\ne 0\right)\right)$$
41	20 33 40	mp2an	$$⊢\left\{A,B\right\}\mathrm{linDepS}Z\leftrightarrow \exists x\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)\left({finSupp}_0\left(x\right)\wedge x\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z\wedge \exists y\in \left\{A,B\right\}x\left(y\right)\ne 0\right)$$
42	18 41	mpbir	$$⊢\left\{A,B\right\}\mathrm{linDepS}Z$$