Theorem ldepsnlinclem2

Description: Lemma 2 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	ldepsnlinclem2	$$⊢F\in \left({{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}}^{\left\{A\right\}}\right)\to F\mathrm{linC}\left(Z\right)\left\{A\right\}\ne B$$

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