Theorem zlmodzxzldeplem3

Description: Lemma 3 for zlmodzxzldep . (Contributed by AV, 24-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\}$$
	zlmodzxzldeplem.f	$$⊢F=\left\{⟨A,2⟩,⟨B,-3⟩\right\}$$
Assertion	zlmodzxzldeplem3	$$⊢F\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_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		zlmodzxzldeplem.f	$$⊢F=\left\{⟨A,2⟩,⟨B,-3⟩\right\}$$
5		ovex	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}\in \mathrm{V}$$
6	1 5	eqeltri	$$⊢Z\in \mathrm{V}$$
7	1 2 3 4	zlmodzxzldeplem1	$$⊢F\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)$$
8	1	zlmodzxzlmod	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)$$
9		simpr	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)$$
10	9	eqcomd	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)\to \mathrm{Scalar}\left(Z\right)={\mathbb{Z}}_{\mathrm{ring}}$$
11	8 10	ax-mp	$$⊢\mathrm{Scalar}\left(Z\right)={\mathbb{Z}}_{\mathrm{ring}}$$
12	11	fveq2i	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
13		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
14	13	eqcomi	$$⊢{\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}=\mathbb{Z}$$
15	12 14	eqtri	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}=\mathbb{Z}$$
16	15	oveq1i	$$⊢{{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}}^{\left\{A,B\right\}}={\mathbb{Z}}^{\left\{A,B\right\}}$$
17	7 16	eleqtrri	$$⊢F\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}}^{\left\{A,B\right\}}\right)$$
18		3z	$$⊢3\in \mathbb{Z}$$
19		6nn	$$⊢6\in \mathbb{N}$$
20	19	nnzi	$$⊢6\in \mathbb{Z}$$
21	1	zlmodzxzel	$$⊢\left(3\in \mathbb{Z}\wedge 6\in \mathbb{Z}\right)\to \left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_Z$$
22	18 20 21	mp2an	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_Z$$
23		2z	$$⊢2\in \mathbb{Z}$$
24		4z	$$⊢4\in \mathbb{Z}$$
25	1	zlmodzxzel	$$⊢\left(2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
26	23 24 25	mp2an	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
27	2	eleq1i	$$⊢A\in {\mathrm{Base}}_Z\leftrightarrow \left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_Z$$
28	3	eleq1i	$$⊢B\in {\mathrm{Base}}_Z\leftrightarrow \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z$$
29	27 28	anbi12i	$$⊢\left(A\in {\mathrm{Base}}_Z\wedge B\in {\mathrm{Base}}_Z\right)\leftrightarrow \left(\left\{⟨0,3⟩,⟨1,6⟩\right\}\in {\mathrm{Base}}_Z\wedge \left\{⟨0,2⟩,⟨1,4⟩\right\}\in {\mathrm{Base}}_Z\right)$$
30	22 26 29	mpbir2an	$$⊢\left(A\in {\mathrm{Base}}_Z\wedge B\in {\mathrm{Base}}_Z\right)$$
31		prelpwi	$$⊢\left(A\in {\mathrm{Base}}_Z\wedge B\in {\mathrm{Base}}_Z\right)\to \left\{A,B\right\}\in 𝒫{\mathrm{Base}}_Z$$
32	30 31	ax-mp	$$⊢\left\{A,B\right\}\in 𝒫{\mathrm{Base}}_Z$$
33		lincval	$$⊢\left(Z\in \mathrm{V}\wedge F\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}}^{\left\{A,B\right\}}\right)\wedge \left\{A,B\right\}\in 𝒫{\mathrm{Base}}_Z\right)\to F\mathrm{linC}\left(Z\right)\left\{A,B\right\}=\underset{x\in \left\{A,B\right\}}{{\sum }_Z}\left(F\left(x\right){\cdot }_{Z}x\right)$$
34	6 17 32 33	mp3an	$$⊢F\mathrm{linC}\left(Z\right)\left\{A,B\right\}=\underset{x\in \left\{A,B\right\}}{{\sum }_Z}\left(F\left(x\right){\cdot }_{Z}x\right)$$
35		lmodcmn	$$⊢Z\in \mathrm{LMod}\to Z\in \mathrm{CMnd}$$
36	35	adantr	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)\to Z\in \mathrm{CMnd}$$
37	8 36	ax-mp	$$⊢Z\in \mathrm{CMnd}$$
38		prex	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\in \mathrm{V}$$
39	2 38	eqeltri	$$⊢A\in \mathrm{V}$$
40		prex	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in \mathrm{V}$$
41	3 40	eqeltri	$$⊢B\in \mathrm{V}$$
42	1 2 3	zlmodzxzldeplem	$$⊢A\ne B$$
43	39 41 42	3pm3.2i	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)$$
44	8	simpli	$$⊢Z\in \mathrm{LMod}$$
45		elmapi	$$⊢F\in \left({\mathbb{Z}}^{\left\{A,B\right\}}\right)\to F:\left\{A,B\right\}⟶\mathbb{Z}$$
46	39	prid1	$$⊢A\in \left\{A,B\right\}$$
47		ffvelrn	$$⊢\left(F:\left\{A,B\right\}⟶\mathbb{Z}\wedge A\in \left\{A,B\right\}\right)\to F\left(A\right)\in \mathbb{Z}$$
48	46 47	mpan2	$$⊢F:\left\{A,B\right\}⟶\mathbb{Z}\to F\left(A\right)\in \mathbb{Z}$$
49	7 45 48	mp2b	$$⊢F\left(A\right)\in \mathbb{Z}$$
50	8 9	ax-mp	$$⊢{\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)$$
51	50	eqcomi	$$⊢\mathrm{Scalar}\left(Z\right)={\mathbb{Z}}_{\mathrm{ring}}$$
52	51	fveq2i	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
53	52 14	eqtri	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}=\mathbb{Z}$$
54	49 53	eleqtrri	$$⊢F\left(A\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}$$
55	2 22	eqeltri	$$⊢A\in {\mathrm{Base}}_Z$$
56		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
57		eqid	$$⊢\mathrm{Scalar}\left(Z\right)=\mathrm{Scalar}\left(Z\right)$$
58		eqid	$$⊢{\cdot }_Z={\cdot }_Z$$
59		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}$$
60	56 57 58 59	lmodvscl	$$⊢\left(Z\in \mathrm{LMod}\wedge F\left(A\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}\wedge A\in {\mathrm{Base}}_Z\right)\to F\left(A\right){\cdot }_{Z}A\in {\mathrm{Base}}_Z$$
61	44 54 55 60	mp3an	$$⊢F\left(A\right){\cdot }_{Z}A\in {\mathrm{Base}}_Z$$
62	41	prid2	$$⊢B\in \left\{A,B\right\}$$
63		ffvelrn	$$⊢\left(F:\left\{A,B\right\}⟶\mathbb{Z}\wedge B\in \left\{A,B\right\}\right)\to F\left(B\right)\in \mathbb{Z}$$
64	62 63	mpan2	$$⊢F:\left\{A,B\right\}⟶\mathbb{Z}\to F\left(B\right)\in \mathbb{Z}$$
65	7 45 64	mp2b	$$⊢F\left(B\right)\in \mathbb{Z}$$
66	65 53	eleqtrri	$$⊢F\left(B\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}$$
67	3 26	eqeltri	$$⊢B\in {\mathrm{Base}}_Z$$
68	56 57 58 59	lmodvscl	$$⊢\left(Z\in \mathrm{LMod}\wedge F\left(B\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(Z\right)}\wedge B\in {\mathrm{Base}}_Z\right)\to F\left(B\right){\cdot }_{Z}B\in {\mathrm{Base}}_Z$$
69	44 66 67 68	mp3an	$$⊢F\left(B\right){\cdot }_{Z}B\in {\mathrm{Base}}_Z$$
70	61 69	pm3.2i	$$⊢\left(F\left(A\right){\cdot }_{Z}A\in {\mathrm{Base}}_Z\wedge F\left(B\right){\cdot }_{Z}B\in {\mathrm{Base}}_Z\right)$$
71		eqid	$$⊢{+}_Z={+}_Z$$
72		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
73		id	$$⊢x=A\to x=A$$
74	72 73	oveq12d	$$⊢x=A\to F\left(x\right){\cdot }_{Z}x=F\left(A\right){\cdot }_{Z}A$$
75		fveq2	$$⊢x=B\to F\left(x\right)=F\left(B\right)$$
76		id	$$⊢x=B\to x=B$$
77	75 76	oveq12d	$$⊢x=B\to F\left(x\right){\cdot }_{Z}x=F\left(B\right){\cdot }_{Z}B$$
78	56 71 74 77	gsumpr	$$⊢\left(Z\in \mathrm{CMnd}\wedge \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\wedge \left(F\left(A\right){\cdot }_{Z}A\in {\mathrm{Base}}_Z\wedge F\left(B\right){\cdot }_{Z}B\in {\mathrm{Base}}_Z\right)\right)\to \underset{x\in \left\{A,B\right\}}{{\sum }_Z}\left(F\left(x\right){\cdot }_{Z}x\right)=\left(F\left(A\right){\cdot }_{Z}A\right){+}_Z\left(F\left(B\right){\cdot }_{Z}B\right)$$
79	37 43 70 78	mp3an	$$⊢\underset{x\in \left\{A,B\right\}}{{\sum }_Z}\left(F\left(x\right){\cdot }_{Z}x\right)=\left(F\left(A\right){\cdot }_{Z}A\right){+}_Z\left(F\left(B\right){\cdot }_{Z}B\right)$$
80	4	fveq1i	$$⊢F\left(A\right)=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(A\right)$$
81		2ex	$$⊢2\in \mathrm{V}$$
82	39 81	fvpr1	$$⊢A\ne B\to \left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(A\right)=2$$
83	42 82	ax-mp	$$⊢\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(A\right)=2$$
84	80 83	eqtri	$$⊢F\left(A\right)=2$$
85	84	oveq1i	$$⊢F\left(A\right){\cdot }_{Z}A=2{\cdot }_{Z}A$$
86	4	fveq1i	$$⊢F\left(B\right)=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(B\right)$$
87		negex	$$⊢-3\in \mathrm{V}$$
88	41 87	fvpr2	$$⊢A\ne B\to \left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(B\right)=-3$$
89	42 88	ax-mp	$$⊢\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(B\right)=-3$$
90	86 89	eqtri	$$⊢F\left(B\right)=-3$$
91	90	oveq1i	$$⊢F\left(B\right){\cdot }_{Z}B=-3{\cdot }_{Z}B$$
92	85 91	oveq12i	$$⊢\left(F\left(A\right){\cdot }_{Z}A\right){+}_Z\left(F\left(B\right){\cdot }_{Z}B\right)=\left(2{\cdot }_{Z}A\right){+}_Z\left(-3{\cdot }_{Z}B\right)$$
93		eqid	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
94	1 93	zlmodzxz0	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}=0_Z$$
95	94	eqcomi	$$⊢0_Z=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
96	1 2 3 95 71 58	zlmodzxzequap	$$⊢\left(2{\cdot }_{Z}A\right){+}_Z\left(-3{\cdot }_{Z}B\right)=0_Z$$
97	92 96	eqtri	$$⊢\left(F\left(A\right){\cdot }_{Z}A\right){+}_Z\left(F\left(B\right){\cdot }_{Z}B\right)=0_Z$$
98	34 79 97	3eqtri	$$⊢F\mathrm{linC}\left(Z\right)\left\{A,B\right\}=0_Z$$