This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ↔ 𝑃 ≠ 𝑄 ) )