Metamath Proof Explorer

Theorem lhpat

Description: Create an atom under a co-atom. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 23-May-2012)

Ref Expression
Hypotheses lhpat.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpat.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpat.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 lhpat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lhpat.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 lhpat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lhpat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝐾 ∈ HL )
7 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ∈ 𝐴 )
8 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑄 ∈ 𝐴 )
9 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑊 ∈ 𝐻 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
12 9 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
13 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ≠ 𝑄 )
14 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
15 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
16 14 15 5 lhp1cvr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
17 16 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
18 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → ¬ 𝑃 ≤ 𝑊 )
19 10 1 2 3 14 15 4 1cvrat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 )
20 6 7 8 12 13 17 18 19 syl133anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ 𝐴 )