Theorem zlmodzxzldeplem2

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

	Ref	Expression
Hypotheses	zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
	zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
	zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
	zlmodzxzldeplem.f	⊢ 𝐹 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ }
Assertion	zlmodzxzldeplem2	⊢ 𝐹 finSupp 0

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
3		zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
4		zlmodzxzldeplem.f	⊢ 𝐹 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ }
5	1 2 3 4	zlmodzxzldeplem1	⊢ 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } )
6		elmapi	⊢ ( 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ )
7		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
8	7	a1i	⊢ ( 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) → { 𝐴 , 𝐵 } ∈ Fin )
9		c0ex	⊢ 0 ∈ V
10	9	a1i	⊢ ( 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) → 0 ∈ V )
11	6 8 10	fdmfifsupp	⊢ ( 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) → 𝐹 finSupp 0 )
12	5 11	ax-mp	⊢ 𝐹 finSupp 0