Theorem zlmodzxzldeplem2

Description: Lemma 2 for zlmodzxzldep . (Contributed by AV, 24-May-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	zlmodzxzldep.z	|- Z = ( ZZring freeLMod { 0 , 1 } )
	zlmodzxzldep.a	|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
	zlmodzxzldep.b	|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
	zlmodzxzldeplem.f	|- F = { <. A , 2 >. , <. B , -u 3 >. }
Assertion	zlmodzxzldeplem2	|- F finSupp 0

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	|- Z = ( ZZring freeLMod { 0 , 1 } )
2		zlmodzxzldep.a	|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
3		zlmodzxzldep.b	|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
4		zlmodzxzldeplem.f	|- F = { <. A , 2 >. , <. B , -u 3 >. }
5	1 2 3 4	zlmodzxzldeplem1	|- F e. ( ZZ ^m { A , B } )
6		elmapi	|- ( F e. ( ZZ ^m { A , B } ) -> F : { A , B } --> ZZ )
7		prfi	|- { A , B } e. Fin
8	7	a1i	|- ( F e. ( ZZ ^m { A , B } ) -> { A , B } e. Fin )
9		c0ex	|- 0 e. _V
10	9	a1i	|- ( F e. ( ZZ ^m { A , B } ) -> 0 e. _V )
11	6 8 10	fdmfifsupp	|- ( F e. ( ZZ ^m { A , B } ) -> F finSupp 0 )
12	5 11	ax-mp	|- F finSupp 0