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

Theorem 4at 33178
 Description: Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 33042 and 3at 33055. (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 33177 . 2
5 simp11 1038 . . . . . 6
6 hllat 32929 . . . . . 6
75, 6syl 17 . . . . 5
8 simp23 1043 . . . . . . 7
9 simp31 1044 . . . . . . 7
10 eqid 2451 . . . . . . . 8
1110, 2, 3hlatjcl 32932 . . . . . . 7
125, 8, 9, 11syl3anc 1268 . . . . . 6
13 simp32 1045 . . . . . . 7
14 simp33 1046 . . . . . . 7
1510, 2, 3hlatjcl 32932 . . . . . . 7
165, 13, 14, 15syl3anc 1268 . . . . . 6
1710, 2latjcl 16297 . . . . . 6
187, 12, 16, 17syl3anc 1268 . . . . 5
1910, 1latref 16299 . . . . 5
207, 18, 19syl2anc 667 . . . 4
21 breq1 4405 . . . 4
2220, 21syl5ibrcom 226 . . 3