Theorem zlmodzxzldeplem1

Description: Lemma 1 for zlmodzxzldep . (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-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	zlmodzxzldeplem1	⊢ 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } )

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		zex	⊢ ℤ ∈ V
6		prex	⊢ { 𝐴 , 𝐵 } ∈ V
7		prex	⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ V
8	2 7	eqeltri	⊢ 𝐴 ∈ V
9		prex	⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ V
10	3 9	eqeltri	⊢ 𝐵 ∈ V
11	8 10	pm3.2i	⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
12	11	a1i	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
13		2z	⊢ 2 ∈ ℤ
14		3nn0	⊢ 3 ∈ ℕ0
15	14	nn0negzi	⊢ - 3 ∈ ℤ
16	13 15	pm3.2i	⊢ ( 2 ∈ ℤ ∧ - 3 ∈ ℤ )
17	16	a1i	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → ( 2 ∈ ℤ ∧ - 3 ∈ ℤ ) )
18	1 2 3	zlmodzxzldeplem	⊢ 𝐴 ≠ 𝐵
19	18	a1i	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → 𝐴 ≠ 𝐵 )
20		fprg	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 2 ∈ ℤ ∧ - 3 ∈ ℤ ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 2 , - 3 } )
21	4	feq1i	⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ { 2 , - 3 } ↔ { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 2 , - 3 } )
22	20 21	sylibr	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 2 ∈ ℤ ∧ - 3 ∈ ℤ ) ∧ 𝐴 ≠ 𝐵 ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ { 2 , - 3 } )
23	12 17 19 22	syl3anc	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ { 2 , - 3 } )
24		prssi	⊢ ( ( 2 ∈ ℤ ∧ - 3 ∈ ℤ ) → { 2 , - 3 } ⊆ ℤ )
25	13 15 24	mp2an	⊢ { 2 , - 3 } ⊆ ℤ
26		fss	⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ { 2 , - 3 } ∧ { 2 , - 3 } ⊆ ℤ ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ )
27	23 25 26	sylancl	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ )
28		elmapg	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → ( 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) ↔ 𝐹 : { 𝐴 , 𝐵 } ⟶ ℤ ) )
29	27 28	mpbird	⊢ ( ( ℤ ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) → 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) )
30	5 6 29	mp2an	⊢ 𝐹 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } )