Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  4at Unicode version

Theorem 4at 29802
 Description: Four atoms determine a lattice volume uniquely. Three-dimensional analog of ps-1 29666 and 3at 29679. (Contributed by NM, 11-Jul-2012.)
Hypotheses
Ref Expression
4at.l
4at.j
4at.a
Assertion
Ref Expression
4at

Proof of Theorem 4at
StepHypRef Expression
1 4at.l . . 3
2 4at.j . . 3
3 4at.a . . 3
41, 2, 34atlem12 29801 . 2
5 simp11 985 . . . . . 6
6 hllat 29553 . . . . . 6
75, 6syl 15 . . . . 5
8 simp23 990 . . . . . . 7
9 simp31 991 . . . . . . 7
10 eqid 2283 . . . . . . . 8
1110, 2, 3hlatjcl 29556 . . . . . . 7
125, 8, 9, 11syl3anc 1182 . . . . . 6
13 simp32 992 . . . . . . 7
14 simp33 993 . . . . . . 7
1510, 2, 3hlatjcl 29556 . . . . . . 7
165, 13, 14, 15syl3anc 1182 . . . . . 6
1710, 2latjcl 14156 . . . . . 6
187, 12, 16, 17syl3anc 1182 . . . . 5
1910, 1latref 14159 . . . . 5
207, 18, 19syl2anc 642 . . . 4
21 breq1 4026 . . . 4
2220, 21syl5ibrcom 213 . . 3