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 ‘ 𝐾 )
3at.j = ( join ‘ 𝐾 )
3at.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3at ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ↔ ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 3at.l = ( le ‘ 𝐾 )
2 3at.j = ( join ‘ 𝐾 )
3 3at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 3atlem7 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )
5 4 3expia ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) ) )
6 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 simpl ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝐾 ∈ Lat )
8 simpr1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑃𝐴 )
9 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
11 8 10 syl ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
12 simpr2 ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑄𝐴 )
13 9 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
15 9 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
16 7 11 14 15 syl3anc ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
17 simpr3 ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑅𝐴 )
18 9 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
19 17 18 syl ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
20 9 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
21 7 16 19 20 syl3anc ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
22 9 1 latref ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
23 21 22 syldan ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
24 breq2 ( ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑃 𝑄 ) 𝑅 ) ↔ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
25 23 24 syl5ibcom ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
26 6 25 sylan ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
27 26 3adant3 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
28 27 adantr ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
29 5 28 impbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ) → ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ↔ ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) ) )