Metamath Proof Explorer


Theorem 1dimN

Description: An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2dim.j = ( join ‘ 𝐾 )
2dim.c 𝐶 = ( ⋖ ‘ 𝐾 )
2dim.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 1dimN ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ∃ 𝑞𝐴 𝑃 𝐶 ( 𝑃 𝑞 ) )

Proof

Step Hyp Ref Expression
1 2dim.j = ( join ‘ 𝐾 )
2 2dim.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 2dim.a 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 2dim ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ∃ 𝑞𝐴𝑟𝐴 ( 𝑃 𝐶 ( 𝑃 𝑞 ) ∧ ( 𝑃 𝑞 ) 𝐶 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
5 r19.42v ( ∃ 𝑟𝐴 ( 𝑃 𝐶 ( 𝑃 𝑞 ) ∧ ( 𝑃 𝑞 ) 𝐶 ( ( 𝑃 𝑞 ) 𝑟 ) ) ↔ ( 𝑃 𝐶 ( 𝑃 𝑞 ) ∧ ∃ 𝑟𝐴 ( 𝑃 𝑞 ) 𝐶 ( ( 𝑃 𝑞 ) 𝑟 ) ) )
6 5 simplbi ( ∃ 𝑟𝐴 ( 𝑃 𝐶 ( 𝑃 𝑞 ) ∧ ( 𝑃 𝑞 ) 𝐶 ( ( 𝑃 𝑞 ) 𝑟 ) ) → 𝑃 𝐶 ( 𝑃 𝑞 ) )
7 6 reximi ( ∃ 𝑞𝐴𝑟𝐴 ( 𝑃 𝐶 ( 𝑃 𝑞 ) ∧ ( 𝑃 𝑞 ) 𝐶 ( ( 𝑃 𝑞 ) 𝑟 ) ) → ∃ 𝑞𝐴 𝑃 𝐶 ( 𝑃 𝑞 ) )
8 4 7 syl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴 ) → ∃ 𝑞𝐴 𝑃 𝐶 ( 𝑃 𝑞 ) )