Metamath Proof Explorer


Theorem lhpex2leN

Description: There exist at least two different atoms under a co-atom. This allows us to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhp2at.l = ( le ‘ 𝐾 )
lhp2at.a 𝐴 = ( Atoms ‘ 𝐾 )
lhp2at.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpex2leN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴𝑞𝐴 ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) )

Proof

Step Hyp Ref Expression
1 lhp2at.l = ( le ‘ 𝐾 )
2 lhp2at.a 𝐴 = ( Atoms ‘ 𝐾 )
3 lhp2at.h 𝐻 = ( LHyp ‘ 𝐾 )
4 simprr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑝 𝑊 ) ) → 𝑝 𝑊 )
5 1 2 3 lhpexle1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑞𝐴 ( 𝑞 𝑊𝑞𝑝 ) )
6 5 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑝 𝑊 ) ) → ∃ 𝑞𝐴 ( 𝑞 𝑊𝑞𝑝 ) )
7 4 6 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑝 𝑊 ) ) → ( 𝑝 𝑊 ∧ ∃ 𝑞𝐴 ( 𝑞 𝑊𝑞𝑝 ) ) )
8 necom ( 𝑝𝑞𝑞𝑝 )
9 8 3anbi3i ( ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) ↔ ( 𝑝 𝑊𝑞 𝑊𝑞𝑝 ) )
10 3anass ( ( 𝑝 𝑊𝑞 𝑊𝑞𝑝 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑞 𝑊𝑞𝑝 ) ) )
11 9 10 bitri ( ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑞 𝑊𝑞𝑝 ) ) )
12 11 rexbii ( ∃ 𝑞𝐴 ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) ↔ ∃ 𝑞𝐴 ( 𝑝 𝑊 ∧ ( 𝑞 𝑊𝑞𝑝 ) ) )
13 r19.42v ( ∃ 𝑞𝐴 ( 𝑝 𝑊 ∧ ( 𝑞 𝑊𝑞𝑝 ) ) ↔ ( 𝑝 𝑊 ∧ ∃ 𝑞𝐴 ( 𝑞 𝑊𝑞𝑝 ) ) )
14 12 13 bitr2i ( ( 𝑝 𝑊 ∧ ∃ 𝑞𝐴 ( 𝑞 𝑊𝑞𝑝 ) ) ↔ ∃ 𝑞𝐴 ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) )
15 7 14 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑝 𝑊 ) ) → ∃ 𝑞𝐴 ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) )
16 1 2 3 lhpexle ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 𝑝 𝑊 )
17 15 16 reximddv ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴𝑞𝐴 ( 𝑝 𝑊𝑞 𝑊𝑝𝑞 ) )