Theorem ldepsnlinclem1

Description: Lemma 1 for ldepsnlinc . (Contributed by AV, 25-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	ldepsnlinclem1	$$⊢F\in \left({{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{B\right\}}\right)\to F\mathrm{linC}\left(Z\right)\left\{B\right\}\ne A$$

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		elmapi	$$⊢F\in \left({{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{B\right\}}\right)\to F:\left\{B\right\}⟶{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
5		prex	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in \mathrm{V}$$
6	3 5	eqeltri	$$⊢B\in \mathrm{V}$$
7	6	fsn2	$$⊢F:\left\{B\right\}⟶{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\leftrightarrow \left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)$$
8		oveq1	$$⊢F=\left\{⟨B,F\left(B\right)⟩\right\}\to F\mathrm{linC}\left(Z\right)\left\{B\right\}=\left\{⟨B,F\left(B\right)⟩\right\}\mathrm{linC}\left(Z\right)\left\{B\right\}$$
9	8	adantl	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\mathrm{linC}\left(Z\right)\left\{B\right\}=\left\{⟨B,F\left(B\right)⟩\right\}\mathrm{linC}\left(Z\right)\left\{B\right\}$$
10	1	zlmodzxzlmod	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)$$
11	10	simpli	$$⊢Z\in \mathrm{LMod}$$
12	11	a1i	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to Z\in \mathrm{LMod}$$
13		2z	$$⊢2\in \mathbb{Z}$$
14		4z	$$⊢4\in \mathbb{Z}$$
15	1	zlmodzxzel	$$⊢\left(2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
16	13 14 15	mp2an	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
17	3 16	eqeltri	$$⊢B\in {\mathrm{Base}}_Z$$
18	17	a1i	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to B\in {\mathrm{Base}}_Z$$
19		simpl	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
20		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
21	10	simpri	$$⊢{\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)$$
22		eqid	$$⊢{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
23		eqid	$$⊢{\cdot }_Z={\cdot }_Z$$
24	20 21 22 23	lincvalsng	$$⊢\left(Z\in \mathrm{LMod}\wedge B\in {\mathrm{Base}}_Z\wedge F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\to \left\{⟨B,F\left(B\right)⟩\right\}\mathrm{linC}\left(Z\right)\left\{B\right\}=F\left(B\right){\cdot }_{Z}B$$
25	12 18 19 24	syl3anc	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to \left\{⟨B,F\left(B\right)⟩\right\}\mathrm{linC}\left(Z\right)\left\{B\right\}=F\left(B\right){\cdot }_{Z}B$$
26	9 25	eqtrd	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\mathrm{linC}\left(Z\right)\left\{B\right\}=F\left(B\right){\cdot }_{Z}B$$
27		eqid	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
28		eqid	$$⊢{-}_Z={-}_Z$$
29	1 27 23 28 2 3	zlmodzxznm	$$⊢\forall i\in \mathbb{Z}\left(i{\cdot }_{Z}A\ne B\wedge i{\cdot }_{Z}B\ne A\right)$$
30		r19.26	$$⊢\forall i\in \mathbb{Z}\left(i{\cdot }_{Z}A\ne B\wedge i{\cdot }_{Z}B\ne A\right)\leftrightarrow \left(\forall i\in \mathbb{Z}i{\cdot }_{Z}A\ne B\wedge \forall i\in \mathbb{Z}i{\cdot }_{Z}B\ne A\right)$$
31		oveq1	$$⊢i=F\left(B\right)\to i{\cdot }_{Z}B=F\left(B\right){\cdot }_{Z}B$$
32	31	neeq1d	$$⊢i=F\left(B\right)\to \left(i{\cdot }_{Z}B\ne A\leftrightarrow F\left(B\right){\cdot }_{Z}B\ne A\right)$$
33	32	rspcv	$$⊢F\left(B\right)\in \mathbb{Z}\to \left(\forall i\in \mathbb{Z}i{\cdot }_{Z}B\ne A\to F\left(B\right){\cdot }_{Z}B\ne A\right)$$
34		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
35	34	eqcomi	$$⊢{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}=\mathbb{Z}$$
36	35	eleq2i	$$⊢F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\leftrightarrow F\left(B\right)\in \mathbb{Z}$$
37	36	birani	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\left(B\right)\in \mathbb{Z}$$
38	33 37	syl11	$$⊢\forall i\in \mathbb{Z}i{\cdot }_{Z}B\ne A\to \left(\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\left(B\right){\cdot }_{Z}B\ne A\right)$$
39	38	adantl	$$⊢\left(\forall i\in \mathbb{Z}i{\cdot }_{Z}A\ne B\wedge \forall i\in \mathbb{Z}i{\cdot }_{Z}B\ne A\right)\to \left(\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\left(B\right){\cdot }_{Z}B\ne A\right)$$
40	30 39	sylbi	$$⊢\forall i\in \mathbb{Z}\left(i{\cdot }_{Z}A\ne B\wedge i{\cdot }_{Z}B\ne A\right)\to \left(\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\left(B\right){\cdot }_{Z}B\ne A\right)$$
41	29 40	ax-mp	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\left(B\right){\cdot }_{Z}B\ne A$$
42	26 41	eqnetrd	$$⊢\left(F\left(B\right)\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge F=\left\{⟨B,F\left(B\right)⟩\right\}\right)\to F\mathrm{linC}\left(Z\right)\left\{B\right\}\ne A$$
43	7 42	sylbi	$$⊢F:\left\{B\right\}⟶{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\to F\mathrm{linC}\left(Z\right)\left\{B\right\}\ne A$$
44	4 43	syl	$$⊢F\in \left({{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{B\right\}}\right)\to F\mathrm{linC}\left(Z\right)\left\{B\right\}\ne A$$