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

Metamath Proof Explorer

Theorem 2lplnm2N

Description: The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2lplnm2.l 
|- .<_ = ( le ` K )
2lplnm2.m 
|- ./\ = ( meet ` K )
2lplnm2.a 
|- N = ( LLines ` K )
2lplnm2.p 
|- P = ( LPlanes ` K )
2lplnm2.v 
|- V = ( LVols ` K )
Assertion 2lplnm2N 
|- ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ./\ Y ) e. N )

Proof

Step Hyp Ref Expression
1 2lplnm2.l 
 |-  .<_ = ( le ` K )
2 2lplnm2.m 
 |-  ./\ = ( meet ` K )
3 2lplnm2.a 
 |-  N = ( LLines ` K )
4 2lplnm2.p 
 |-  P = ( LPlanes ` K )
5 2lplnm2.v 
 |-  V = ( LVols ` K )
6 simp22 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> Y e. P )
7 simp1 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> K e. HL )
8 hllat 
 |-  ( K e. HL -> K e. Lat )
9 8 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> K e. Lat )
10 simp21 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> X e. P )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 4 lplnbase 
 |-  ( X e. P -> X e. ( Base ` K ) )
13 10 12 syl 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> X e. ( Base ` K ) )
14 11 4 lplnbase 
 |-  ( Y e. P -> Y e. ( Base ` K ) )
15 6 14 syl 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> Y e. ( Base ` K ) )
16 11 2 latmcl 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
17 9 13 15 16 syl3anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
18 eqid 
 |-  ( join ` K ) = ( join ` K )
19 1 18 4 5 2lplnj 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ( join ` K ) Y ) = W )
20 simp23 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> W e. V )
21 19 20 eqeltrd 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ( join ` K ) Y ) e. V )
22 11 1 18 latlej1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> X .<_ ( X ( join ` K ) Y ) )
23 9 13 15 22 syl3anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> X .<_ ( X ( join ` K ) Y ) )
24 eqid 
 |-  (
25 1 24 4 5 lplncvrlvol2 
 |-  ( ( ( K e. HL /\ X e. P /\ ( X ( join ` K ) Y ) e. V ) /\ X .<_ ( X ( join ` K ) Y ) ) -> X (
26 7 10 21 23 25 syl31anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> X (
27 11 18 2 24 cvrexch 
 |-  ( ( K e. HL /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( ( X ./\ Y ) (  X (
28 7 13 15 27 syl3anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( X ./\ Y ) (  X (
29 26 28 mpbird 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ./\ Y ) (
30 11 24 3 4 llncvrlpln 
 |-  ( ( ( K e. HL /\ ( X ./\ Y ) e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ ( X ./\ Y ) (  ( ( X ./\ Y ) e. N <-> Y e. P ) )
31 7 17 15 29 30 syl31anc 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( X ./\ Y ) e. N <-> Y e. P ) )
32 6 31 mpbird 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ./\ Y ) e. N )