Metamath Proof Explorer


Theorem 2lplnmN

Description: If the join of two lattice planes covers one of them, their meet is a lattice line. (Contributed by NM, 30-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2lplnm.j
|- .\/ = ( join ` K )
2lplnm.m
|- ./\ = ( meet ` K )
2lplnm.c
|- C = ( 
2lplnm.n
|- N = ( LLines ` K )
2lplnm.p
|- P = ( LPlanes ` K )
Assertion 2lplnmN
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) e. N )

Proof

Step Hyp Ref Expression
1 2lplnm.j
 |-  .\/ = ( join ` K )
2 2lplnm.m
 |-  ./\ = ( meet ` K )
3 2lplnm.c
 |-  C = ( 
4 2lplnm.n
 |-  N = ( LLines ` K )
5 2lplnm.p
 |-  P = ( LPlanes ` K )
6 simpl3
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> Y e. P )
7 simpl1
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> K e. HL )
8 hllat
 |-  ( K e. HL -> K e. Lat )
9 eqid
 |-  ( Base ` K ) = ( Base ` K )
10 9 5 lplnbase
 |-  ( X e. P -> X e. ( Base ` K ) )
11 9 5 lplnbase
 |-  ( Y e. P -> Y e. ( Base ` K ) )
12 9 2 latmcl
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
13 8 10 11 12 syl3an
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X ./\ Y ) e. ( Base ` K ) )
14 13 adantr
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
15 11 3ad2ant3
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> Y e. ( Base ` K ) )
16 15 adantr
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> Y e. ( Base ` K ) )
17 simp1
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> K e. HL )
18 10 3ad2ant2
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> X e. ( Base ` K ) )
19 9 1 2 3 cvrexch
 |-  ( ( K e. HL /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( ( X ./\ Y ) C Y <-> X C ( X .\/ Y ) ) )
20 17 18 15 19 syl3anc
 |-  ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( ( X ./\ Y ) C Y <-> X C ( X .\/ Y ) ) )
21 20 biimpar
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) C Y )
22 9 3 4 5 llncvrlpln
 |-  ( ( ( K e. HL /\ ( X ./\ Y ) e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ ( X ./\ Y ) C Y ) -> ( ( X ./\ Y ) e. N <-> Y e. P ) )
23 7 14 16 21 22 syl31anc
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( ( X ./\ Y ) e. N <-> Y e. P ) )
24 6 23 mpbird
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) e. N )