# Metamath Proof Explorer

## Theorem 2lplnj

Description: The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses 2lplnj.l
2lplnj.j
2lplnj.p ${⊢}{P}=\mathrm{LPlanes}\left({K}\right)$
2lplnj.v ${⊢}{V}=\mathrm{LVols}\left({K}\right)$
Assertion 2lplnj

### Proof

Step Hyp Ref Expression
1 2lplnj.l
2 2lplnj.j
3 2lplnj.p ${⊢}{P}=\mathrm{LPlanes}\left({K}\right)$
4 2lplnj.v ${⊢}{V}=\mathrm{LVols}\left({K}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
7 5 1 2 6 3 islpln2
8 simpr
9 7 8 syl6bi
10 5 1 2 6 3 islpln2
11 simpr
12 10 11 syl6bi
13 9 12 anim12d
14 13 imp
17 simpl33
19 simp33
20 18 19 oveq12d
21 simp11
22 simp123
23 21 22 jca
26 simp2l
27 simp2rl
28 simp2rr
29 26 27 28 3jca
32 simpl31
34 simpl32
36 33 35 jca
37 simp1r
38 simp2l
39 simp2r
40 37 38 39 3jca
41 simp31
42 simp32
43 41 42 jca
44 simpl13
46 breq1
47 neeq1
48 46 47 3anbi13d
49 breq1
50 neeq2
51 49 50 3anbi23d
52 48 51 sylan9bb
53 18 19 52 syl2anc
54 45 53 mpbid
55 1 2 6 4 2lplnja
56 25 31 36 40 43 54 55 syl321anc
57 20 56 eqtrd
58 57 3exp
59 58 rexlimdvv
60 59 rexlimdva
61 60 3exp
62 61 expdimp
63 62 rexlimdvv
64 63 rexlimdva
65 64 impd
66 16 65 mpd