Theorem islln2a

Description: The predicate "is a lattice line" in terms of atoms. (Contributed by NM, 15-Jul-2012)

	Ref	Expression
Hypotheses	islln2a.j	⊢ ∨ = ( join ‘ 𝐾 )
	islln2a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	islln2a.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion	islln2a	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ↔ 𝑃 ≠ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		islln2a.j	⊢ ∨ = ( join ‘ 𝐾 )
2		islln2a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		islln2a.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
4		oveq1	⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
5	1 2	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
6	5	3adant2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
7	4 6	sylan9eqr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∨ 𝑄 ) = 𝑄 )
8	2 3	llnneat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝑁 ) → ¬ 𝑄 ∈ 𝐴 )
9	8	adantlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑄 ∈ 𝑁 ) → ¬ 𝑄 ∈ 𝐴 )
10	9	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑄 ∈ 𝑁 → ¬ 𝑄 ∈ 𝐴 ) )
11	10	con2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑄 ∈ 𝐴 → ¬ 𝑄 ∈ 𝑁 ) )
12	11	3impia	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ 𝑄 ∈ 𝑁 )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑄 ∈ 𝑁 )
14	7 13	eqneltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 = 𝑄 ) → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 )
15	14	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 = 𝑄 → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ) )
16	15	necon2ad	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 → 𝑃 ≠ 𝑄 ) )
17	1 2 3	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 )
18	17	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 → ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ) )
19	16 18	impbid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ↔ 𝑃 ≠ 𝑄 ) )