# Metamath Proof Explorer

## Theorem 3dim0

Description: There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012)

Ref Expression
Hypotheses 3dim0.j
3dim0.l
3dim0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion 3dim0

### Proof

Step Hyp Ref Expression
1 3dim0.j
2 3dim0.l
3 3dim0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
5 1 4 3 athgt
6 df-3an
7 simpll1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}\in {A}\wedge {q}\in {A}\right)\wedge {r}\in {A}\right)\wedge {s}\in {A}\right)\to {K}\in \mathrm{HL}$
8 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
9 8 1 3 hlatjcl
11 simplr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}\in {A}\wedge {q}\in {A}\right)\wedge {r}\in {A}\right)\wedge {s}\in {A}\right)\to {r}\in {A}$
12 8 2 1 4 3 cvr1
13 7 10 11 12 syl3anc
14 13 anbi2d
15 7 hllatd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}\in {A}\wedge {q}\in {A}\right)\wedge {r}\in {A}\right)\wedge {s}\in {A}\right)\to {K}\in \mathrm{Lat}$
16 8 3 atbase ${⊢}{r}\in {A}\to {r}\in {\mathrm{Base}}_{{K}}$
17 16 ad2antlr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}\in {A}\wedge {q}\in {A}\right)\wedge {r}\in {A}\right)\wedge {s}\in {A}\right)\to {r}\in {\mathrm{Base}}_{{K}}$
18 8 1 latjcl
19 15 10 17 18 syl3anc
20 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}\in {A}\wedge {q}\in {A}\right)\wedge {r}\in {A}\right)\wedge {s}\in {A}\right)\to {s}\in {A}$
21 8 2 1 4 3 cvr1
22 7 19 20 21 syl3anc
23 14 22 anbi12d
24 6 23 syl5bb
25 24 rexbidva
26 r19.42v
27 anass
28 26 27 bitri
29 25 28 syl6bb
30 29 rexbidva
31 r19.42v
32 30 31 syl6bb
33 1 4 3 atcvr1
34 33 anbi1d
35 32 34 bitrd
36 35 3expb
37 36 2rexbidva
38 5 37 mpbird