Metamath Proof Explorer

Theorem lplnexatN

Description: Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnexat.l 
|- .<_ = ( le ` K )
lplnexat.j 
|- .\/ = ( join ` K )
lplnexat.a 
|- A = ( Atoms ` K )
lplnexat.n 
|- N = ( LLines ` K )
lplnexat.p 
|- P = ( LPlanes ` K )
Assertion lplnexatN 
|- ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> E. q e. A ( -. q .<_ Y /\ X = ( Y .\/ q ) ) )

Proof

Step Hyp Ref Expression
1 lplnexat.l 
 |-  .<_ = ( le ` K )
2 lplnexat.j 
 |-  .\/ = ( join ` K )
3 lplnexat.a 
 |-  A = ( Atoms ` K )
4 lplnexat.n 
 |-  N = ( LLines ` K )
5 lplnexat.p 
 |-  P = ( LPlanes ` K )
6 simp1 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> K e. HL )
7 simp3 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> Y e. N )
8 simp2 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> X e. P )
9 6 7 8 3jca 
 |-  ( ( K e. HL /\ X e. P /\ Y e. N ) -> ( K e. HL /\ Y e. N /\ X e. P ) )
10 eqid 
 |-  (
11 1 10 4 5 llncvrlpln2 
 |-  ( ( ( K e. HL /\ Y e. N /\ X e. P ) /\ Y .<_ X ) -> Y (
12 9 11 sylan 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> Y (
13 simpl1 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> K e. HL )
14 simpl3 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> Y e. N )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 15 4 llnbase 
 |-  ( Y e. N -> Y e. ( Base ` K ) )
17 14 16 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> Y e. ( Base ` K ) )
18 simpl2 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> X e. P )
19 15 5 lplnbase 
 |-  ( X e. P -> X e. ( Base ` K ) )
20 18 19 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> X e. ( Base ` K ) )
21 15 1 2 10 3 cvrval3 
 |-  ( ( K e. HL /\ Y e. ( Base ` K ) /\ X e. ( Base ` K ) ) -> ( Y (  E. q e. A ( -. q .<_ Y /\ ( Y .\/ q ) = X ) ) )
22 13 17 20 21 syl3anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> ( Y (  E. q e. A ( -. q .<_ Y /\ ( Y .\/ q ) = X ) ) )
23 eqcom 
 |-  ( ( Y .\/ q ) = X <-> X = ( Y .\/ q ) )
24 23 anbi2i 
 |-  ( ( -. q .<_ Y /\ ( Y .\/ q ) = X ) <-> ( -. q .<_ Y /\ X = ( Y .\/ q ) ) )
25 24 rexbii 
 |-  ( E. q e. A ( -. q .<_ Y /\ ( Y .\/ q ) = X ) <-> E. q e. A ( -. q .<_ Y /\ X = ( Y .\/ q ) ) )
26 22 25 bitrdi 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> ( Y (  E. q e. A ( -. q .<_ Y /\ X = ( Y .\/ q ) ) ) )
27 12 26 mpbid 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. N ) /\ Y .<_ X ) -> E. q e. A ( -. q .<_ Y /\ X = ( Y .\/ q ) ) )