Theorem zlmodzxzldeplem4

Description: Lemma 4 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	zlmodzxzldeplem4	⊢ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑦 ) ≠ 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		prex	⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ V
6	2 5	eqeltri	⊢ 𝐴 ∈ V
7		prex	⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ V
8	3 7	eqeltri	⊢ 𝐵 ∈ V
9		2ne0	⊢ 2 ≠ 0
10	4	fveq1i	⊢ ( 𝐹 ‘ 𝐴 ) = ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐴 )
11	1 2 3	zlmodzxzldeplem	⊢ 𝐴 ≠ 𝐵
12		2ex	⊢ 2 ∈ V
13	6 12	fvpr1	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐴 ) = 2 )
14	11 13	mp1i	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝐴 ) = 2 )
15	10 14	syl5eq	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = 2 )
16	15	neeq1d	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐹 ‘ 𝐴 ) ≠ 0 ↔ 2 ≠ 0 ) )
17	9 16	mpbiri	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ 𝐴 ) ≠ 0 )
18	17	orcd	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐹 ‘ 𝐴 ) ≠ 0 ∨ ( 𝐹 ‘ 𝐵 ) ≠ 0 ) )
19		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
20	19	neeq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ( 𝐹 ‘ 𝐴 ) ≠ 0 ) )
21		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
22	21	neeq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ( 𝐹 ‘ 𝐵 ) ≠ 0 ) )
23	20 22	rexprg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑦 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝐴 ) ≠ 0 ∨ ( 𝐹 ‘ 𝐵 ) ≠ 0 ) ) )
24	18 23	mpbird	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑦 ) ≠ 0 )
25	6 8 24	mp2an	⊢ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑦 ) ≠ 0