Theorem zlmodzxzel

Description: An element of the (base set of the) ZZ-module ZZ X. ZZ . (Contributed by AV, 21-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypothesis	zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
Assertion	zlmodzxzel	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( Base ‘ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		c0ex	⊢ 0 ∈ V
3		1ex	⊢ 1 ∈ V
4	2 3	pm3.2i	⊢ ( 0 ∈ V ∧ 1 ∈ V )
5		0ne1	⊢ 0 ≠ 1
6		fprg	⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 0 ≠ 1 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } ⟶ { 𝐴 , 𝐵 } )
7	4 5 6	mp3an13	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } ⟶ { 𝐴 , 𝐵 } )
8		prssi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝐴 , 𝐵 } ⊆ ℤ )
9		zringbas	⊢ ℤ = ( Base ‘ ℤring )
10	8 9	sseqtrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝐴 , 𝐵 } ⊆ ( Base ‘ ℤring ) )
11	7 10	fssd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } ⟶ ( Base ‘ ℤring ) )
12		fvex	⊢ ( Base ‘ ℤring ) ∈ V
13		prex	⊢ { 0 , 1 } ∈ V
14	12 13	pm3.2i	⊢ ( ( Base ‘ ℤring ) ∈ V ∧ { 0 , 1 } ∈ V )
15		elmapg	⊢ ( ( ( Base ‘ ℤring ) ∈ V ∧ { 0 , 1 } ∈ V ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( ( Base ‘ ℤring ) ↑m { 0 , 1 } ) ↔ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } ⟶ ( Base ‘ ℤring ) ) )
16	14 15	mp1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( ( Base ‘ ℤring ) ↑m { 0 , 1 } ) ↔ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } : { 0 , 1 } ⟶ ( Base ‘ ℤring ) ) )
17	11 16	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( ( Base ‘ ℤring ) ↑m { 0 , 1 } ) )
18		zringring	⊢ ℤring ∈ Ring
19		prfi	⊢ { 0 , 1 } ∈ Fin
20	18 19	pm3.2i	⊢ ( ℤring ∈ Ring ∧ { 0 , 1 } ∈ Fin )
21		eqid	⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring )
22	1 21	frlmfibas	⊢ ( ( ℤring ∈ Ring ∧ { 0 , 1 } ∈ Fin ) → ( ( Base ‘ ℤring ) ↑m { 0 , 1 } ) = ( Base ‘ 𝑍 ) )
23	20 22	mp1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( Base ‘ ℤring ) ↑m { 0 , 1 } ) = ( Base ‘ 𝑍 ) )
24	17 23	eleqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( Base ‘ 𝑍 ) )