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

Metamath Proof Explorer

Theorem llnmlplnN

Description: The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses llnmlpln.l 
|- .<_ = ( le ` K )
llnmlpln.m 
|- ./\ = ( meet ` K )
llnmlpln.z 
|- .0. = ( 0. ` K )
llnmlpln.a 
|- A = ( Atoms ` K )
llnmlpln.n 
|- N = ( LLines ` K )
llnmlpln.p 
|- P = ( LPlanes ` K )
Assertion llnmlplnN 
|- ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. A )

Proof

Step Hyp Ref Expression
1 llnmlpln.l 
 |-  .<_ = ( le ` K )
2 llnmlpln.m 
 |-  ./\ = ( meet ` K )
3 llnmlpln.z 
 |-  .0. = ( 0. ` K )
4 llnmlpln.a 
 |-  A = ( Atoms ` K )
5 llnmlpln.n 
 |-  N = ( LLines ` K )
6 llnmlpln.p 
 |-  P = ( LPlanes ` K )
7 simprl 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) ) -> -. X .<_ Y )
8 simp11 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> K e. HL )
9 8 hllatd 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> K e. Lat )
10 simp12 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> X e. N )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 5 llnbase 
 |-  ( X e. N -> X e. ( Base ` K ) )
13 10 12 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> X e. ( Base ` K ) )
14 simp13 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> Y e. P )
15 11 6 lplnbase 
 |-  ( Y e. P -> Y e. ( Base ` K ) )
16 14 15 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> Y e. ( Base ` K ) )
17 11 2 latmcl 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
18 9 13 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> ( X ./\ Y ) e. ( Base ` K ) )
19 simp2r 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> ( X ./\ Y ) =/= .0. )
20 simp3 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> -. ( X ./\ Y ) e. A )
21 11 1 3 4 5 llnle 
 |-  ( ( ( K e. HL /\ ( X ./\ Y ) e. ( Base ` K ) ) /\ ( ( X ./\ Y ) =/= .0. /\ -. ( X ./\ Y ) e. A ) ) -> E. u e. N u .<_ ( X ./\ Y ) )
22 8 18 19 20 21 syl22anc 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> E. u e. N u .<_ ( X ./\ Y ) )
23 9 adantr 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> K e. Lat )
24 18 adantr 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
25 13 adantr 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> X e. ( Base ` K ) )
26 11 1 2 latmle1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) .<_ X )
27 9 13 16 26 syl3anc 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> ( X ./\ Y ) .<_ X )
28 27 adantr 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> ( X ./\ Y ) .<_ X )
29 11 5 llnbase 
 |-  ( u e. N -> u e. ( Base ` K ) )
30 29 ad2antrl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> u e. ( Base ` K ) )
31 simprr 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> u .<_ ( X ./\ Y ) )
32 11 1 23 30 24 25 31 28 lattrd 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> u .<_ X )
33 simpl11 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> K e. HL )
34 simprl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> u e. N )
35 simpl12 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> X e. N )
36 1 5 llncmp 
 |-  ( ( K e. HL /\ u e. N /\ X e. N ) -> ( u .<_ X <-> u = X ) )
37 33 34 35 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> ( u .<_ X <-> u = X ) )
38 32 37 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> u = X )
39 38 31 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> X .<_ ( X ./\ Y ) )
40 11 1 23 24 25 28 39 latasymd 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) /\ ( u e. N /\ u .<_ ( X ./\ Y ) ) ) -> ( X ./\ Y ) = X )
41 22 40 rexlimddv 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> ( X ./\ Y ) = X )
42 11 1 2 latleeqm1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )
43 9 13 16 42 syl3anc 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )
44 41 43 mpbird 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) /\ -. ( X ./\ Y ) e. A ) -> X .<_ Y )
45 44 3expia 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( -. ( X ./\ Y ) e. A -> X .<_ Y ) )
46 7 45 mt3d 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ ( -. X .<_ Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. A )