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 ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑃𝑄 ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) ∈ 𝐴 )