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 ) ) )