This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )