Metamath Proof Explorer

Theorem llni2

Description: The join of two different atoms is a lattice line. (Contributed by NM, 26-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 llni2.j ⊢ ∨ = ( join ‘ 𝐾 )
2 llni2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 llni2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
4 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝐴 )
5 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ 𝐴 )
6 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
7 eqidd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑄 ) )
8 neeq1 ⊢ ( 𝑟 = 𝑃 → ( 𝑟 ≠ 𝑠 ↔ 𝑃 ≠ 𝑠 ) )
9 oveq1 ⊢ ( 𝑟 = 𝑃 → ( 𝑟 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑠 ) )
10 9 eqeq2d ⊢ ( 𝑟 = 𝑃 → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑠 ) ) )
11 8 10 anbi12d ⊢ ( 𝑟 = 𝑃 → ( ( 𝑟 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) ↔ ( 𝑃 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑠 ) ) ) )
12 neeq2 ⊢ ( 𝑠 = 𝑄 → ( 𝑃 ≠ 𝑠 ↔ 𝑃 ≠ 𝑄 ) )
13 oveq2 ⊢ ( 𝑠 = 𝑄 → ( 𝑃 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑄 ) )
14 13 eqeq2d ⊢ ( 𝑠 = 𝑄 → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑠 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑄 ) ) )
15 12 14 anbi12d ⊢ ( 𝑠 = 𝑄 → ( ( 𝑃 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑠 ) ) ↔ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑄 ) ) ) )
16 11 15 rspc2ev ⊢ ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑄 ) ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) )
17 4 5 6 7 16 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) )
18 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ HL )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 1 2 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
21 20 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
22 19 1 2 3 islln3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) ) )
23 18 21 22 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑟 ∨ 𝑠 ) ) ) )
24 17 23 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝑁 )