Metamath Proof Explorer

Theorem lnnat

Description: A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 lnnat.j ⊢ ∨ = ( join ‘ 𝐾 )
2 lnnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ HL )
4 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝐴 )
5 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
7 5 6 2 atcvr0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 )
8 3 4 7 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 )
9 1 6 2 atcvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
10 9 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
11 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 5 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
14 3 11 13 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
15 12 2 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
16 4 15 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
17 3 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ Lat )
18 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ 𝐴 )
19 12 2 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
21 12 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
22 17 16 20 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
23 12 6 cvrntr ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 ∧ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ¬ ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
24 3 14 16 22 23 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( ( ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 ∧ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ¬ ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
25 8 10 24 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ¬ ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
26 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) → 𝐾 ∈ HL )
27 5 6 2 atcvr0 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
28 26 27 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
29 25 28 mtand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 )
30 29 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) )
31 1 2 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = 𝑃 )
32 31 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = 𝑃 )
33 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
34 32 33 eqeltrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) ∈ 𝐴 )
35 oveq2 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑃 ) = ( 𝑃 ∨ 𝑄 ) )
36 35 eleq1d ⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ∨ 𝑃 ) ∈ 𝐴 ↔ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) )
37 34 36 syl5ibcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) )
38 37 necon3bd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 → 𝑃 ≠ 𝑄 ) )
39 30 38 impbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) )