Theorem 2atmat0

Description: The meet of two unequal lines (expressed as joins of atoms) is an atom or zero. (Contributed by NM, 2-Dec-2012)

	Ref	Expression
Hypotheses	2atmatz.j	⊢ ∨ = ( join ‘ 𝐾 )
	2atmatz.m	⊢ ∧ = ( meet ‘ 𝐾 )
	2atmatz.z	⊢ 0 = ( 0. ‘ 𝐾 )
	2atmatz.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	2atmat0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		2atmatz.j	⊢ ∨ = ( join ‘ 𝐾 )
2		2atmatz.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		2atmatz.z	⊢ 0 = ( 0. ‘ 𝐾 )
4		2atmatz.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
6		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
7		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑆 ∈ 𝐴 )
8	7	orcd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) )
9		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) )
10	1 2 3 4	2at0mat0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
11	5 6 8 9 10	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )