Metamath Proof Explorer


Theorem 2dim

Description: Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012)

Ref Expression
Hypotheses 2dim.j
|- .\/ = ( join ` K )
2dim.c
|- C = ( 
2dim.a
|- A = ( Atoms ` K )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 2dim.j
 |-  .\/ = ( join ` K )
2 2dim.c
 |-  C = ( 
3 2dim.a
 |-  A = ( Atoms ` K )
4 eqid
 |-  ( le ` K ) = ( le ` K )
5 1 4 3 3dim1
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) )
6 df-3an
 |-  ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) )
7 6 rexbii
 |-  ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> E. s e. A ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) )
8 r19.42v
 |-  ( E. s e. A ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ E. s e. A -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) )
9 7 8 bitri
 |-  ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) <-> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) /\ E. s e. A -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) )
10 9 simplbi
 |-  ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) )
11 simplll
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> K e. HL )
12 hlatl
 |-  ( K e. HL -> K e. AtLat )
13 11 12 syl
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> K e. AtLat )
14 simplr
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> q e. A )
15 simpllr
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> P e. A )
16 4 3 atncmp
 |-  ( ( K e. AtLat /\ q e. A /\ P e. A ) -> ( -. q ( le ` K ) P <-> q =/= P ) )
17 13 14 15 16 syl3anc
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( -. q ( le ` K ) P <-> q =/= P ) )
18 necom
 |-  ( q =/= P <-> P =/= q )
19 17 18 bitr2di
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( P =/= q <-> -. q ( le ` K ) P ) )
20 eqid
 |-  ( Base ` K ) = ( Base ` K )
21 20 3 atbase
 |-  ( P e. A -> P e. ( Base ` K ) )
22 15 21 syl
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> P e. ( Base ` K ) )
23 20 4 1 2 3 cvr1
 |-  ( ( K e. HL /\ P e. ( Base ` K ) /\ q e. A ) -> ( -. q ( le ` K ) P <-> P C ( P .\/ q ) ) )
24 11 22 14 23 syl3anc
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( -. q ( le ` K ) P <-> P C ( P .\/ q ) ) )
25 19 24 bitrd
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( P =/= q <-> P C ( P .\/ q ) ) )
26 20 1 3 hlatjcl
 |-  ( ( K e. HL /\ P e. A /\ q e. A ) -> ( P .\/ q ) e. ( Base ` K ) )
27 11 15 14 26 syl3anc
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( P .\/ q ) e. ( Base ` K ) )
28 simpr
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> r e. A )
29 20 4 1 2 3 cvr1
 |-  ( ( K e. HL /\ ( P .\/ q ) e. ( Base ` K ) /\ r e. A ) -> ( -. r ( le ` K ) ( P .\/ q ) <-> ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )
30 11 27 28 29 syl3anc
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( -. r ( le ` K ) ( P .\/ q ) <-> ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )
31 25 30 anbi12d
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) ) <-> ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) )
32 10 31 syl5ib
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ q e. A ) /\ r e. A ) -> ( E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) )
33 32 reximdva
 |-  ( ( ( K e. HL /\ P e. A ) /\ q e. A ) -> ( E. r e. A E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) )
34 33 reximdva
 |-  ( ( K e. HL /\ P e. A ) -> ( E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r ( le ` K ) ( P .\/ q ) /\ -. s ( le ` K ) ( ( P .\/ q ) .\/ r ) ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) ) )
35 5 34 mpd
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )