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

Metamath Proof Explorer

Theorem 3at

Description: Any three non-colinear atoms in a (lattice) plane determine the plane uniquely. This is the 2-dimensional analogue of ps-1 for lines and 4at for volumes. I could not find this proof in the literature on projective geometry (where it is either given as an axiom or stated as an unproved fact), but it is similar to Theorem 15 of Veblen, "The Foundations of Geometry" (1911), p. 18, which uses different axioms. This proof was written before I became aware of Veblen's, and it is possible that a shorter proof could be obtained by using Veblen's proof for hints. (Contributed by NM, 23-Jun-2012)

Ref Expression
Hypotheses 3at.l 
|- .<_ = ( le ` K )
3at.j 
|- .\/ = ( join ` K )
3at.a 
|- A = ( Atoms ` K )
Assertion 3at 
|- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) ) -> ( ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) <-> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) ) )

Proof

Step Hyp Ref Expression
1 3at.l 
 |-  .<_ = ( le ` K )
2 3at.j 
 |-  .\/ = ( join ` K )
3 3at.a 
 |-  A = ( Atoms ` K )
4 1 2 3 3atlem7 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) /\ ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) )
5 4 3expia 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) ) -> ( ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) ) )
6 hllat 
 |-  ( K e. HL -> K e. Lat )
7 simpl 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> K e. Lat )
8 simpr1 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> P e. A )
9 eqid 
 |-  ( Base ` K ) = ( Base ` K )
10 9 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
11 8 10 syl 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> P e. ( Base ` K ) )
12 simpr2 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> Q e. A )
13 9 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
14 12 13 syl 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> Q e. ( Base ` K ) )
15 9 2 latjcl 
 |-  ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
16 7 11 14 15 syl3anc 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
17 simpr3 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R e. A )
18 9 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
19 17 18 syl 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R e. ( Base ` K ) )
20 9 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
21 7 16 19 20 syl3anc 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
22 9 1 latref 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) .<_ ( ( P .\/ Q ) .\/ R ) )
23 21 22 syldan 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) .<_ ( ( P .\/ Q ) .\/ R ) )
24 breq2 
 |-  ( ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) ) )
25 23 24 syl5ibcom 
 |-  ( ( K e. Lat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) -> ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) ) )
26 6 25 sylan 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) -> ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) ) )
27 26 3adant3 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) -> ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) ) )
28 27 adantr 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) ) -> ( ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) -> ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) ) )
29 5 28 impbid 
 |-  ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) ) -> ( ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ U ) <-> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) ) )