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 ` K )
2dim.c
|- C = ( 
2dim.a
|- A = ( Atoms ` K )
Assertion 1dimN
|- ( ( K e. HL /\ P e. A ) -> E. q e. A P C ( P .\/ q ) )

Proof

Step Hyp Ref Expression
1 2dim.j
 |-  .\/ = ( join ` K )
2 2dim.c
 |-  C = ( 
3 2dim.a
 |-  A = ( Atoms ` K )
4 1 2 3 2dim
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )
5 r19.42v
 |-  ( E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) <-> ( P C ( P .\/ q ) /\ E. r e. A ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )
6 5 simplbi
 |-  ( E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) -> P C ( P .\/ q ) )
7 6 reximi
 |-  ( E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) -> E. q e. A P C ( P .\/ q ) )
8 4 7 syl
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A P C ( P .\/ q ) )