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

Theorem 4at2 30413
 Description: Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.)
Hypotheses
Ref Expression
4at.l
4at.j
4at.a
Assertion
Ref Expression
4at2

Proof of Theorem 4at2
StepHypRef Expression
1 4at.l . . 3
2 4at.j . . 3
3 4at.a . . 3
41, 2, 34at 30412 . 2
5 simp11 988 . . . . . 6
6 hllat 30163 . . . . . 6
75, 6syl 16 . . . . 5
8 eqid 2438 . . . . . . 7
98, 2, 3hlatjcl 30166 . . . . . 6
1093ad2ant1 979 . . . . 5
11 simp21 991 . . . . . 6
128, 3atbase 30089 . . . . . 6
1311, 12syl 16 . . . . 5
14 simp22 992 . . . . . 6
158, 3atbase 30089 . . . . . 6
1614, 15syl 16 . . . . 5
178, 2latjass 14526 . . . . 5
187, 10, 13, 16, 17syl13anc 1187 . . . 4
19 simp23 993 . . . . . 6
20 simp31 994 . . . . . 6
218, 2, 3hlatjcl 30166 . . . . . 6
225, 19, 20, 21syl3anc 1185 . . . . 5
23 simp32 995 . . . . . 6
248, 3atbase 30089 . . . . . 6
2523, 24syl 16 . . . . 5
26 simp33 996 . . . . . 6
278, 3atbase 30089 . . . . . 6
2826, 27syl 16 . . . . 5
298, 2latjass 14526 . . . . 5
307, 22, 25, 28, 29syl13anc 1187 . . . 4
3118, 30breq12d 4227 . . 3