# Metamath Proof Explorer

## Theorem dalem38

Description: Lemma for dath . Plane Y belongs to the 3-dimensional volume G H I c . (Contributed by NM, 5-Aug-2012)

Ref Expression
Hypotheses dalem.ph
dalem.l
dalem.j
dalem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dalem.ps
dalem38.m
dalem38.o ${⊢}{O}=\mathrm{LPlanes}\left({K}\right)$
dalem38.y
dalem38.z
dalem38.g
dalem38.h
dalem38.i
Assertion dalem38

### Proof

Step Hyp Ref Expression
1 dalem.ph
2 dalem.l
3 dalem.j
4 dalem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 dalem.ps
6 dalem38.m
7 dalem38.o ${⊢}{O}=\mathrm{LPlanes}\left({K}\right)$
8 dalem38.y
9 dalem38.z
10 dalem38.g
11 dalem38.h
12 dalem38.i
13 1 2 3 4 5 6 7 8 9 10 dalem28
14 1 2 3 4 5 6 7 8 9 11 dalem33
15 1 dalemkelat ${⊢}{\phi }\to {K}\in \mathrm{Lat}$
16 15 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {K}\in \mathrm{Lat}$
17 1 4 dalempeb ${⊢}{\phi }\to {P}\in {\mathrm{Base}}_{{K}}$
18 17 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {P}\in {\mathrm{Base}}_{{K}}$
19 1 dalemkehl ${⊢}{\phi }\to {K}\in \mathrm{HL}$
20 19 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {K}\in \mathrm{HL}$
21 1 2 3 4 5 6 7 8 9 10 dalem23 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {G}\in {A}$
22 5 dalemccea ${⊢}{\psi }\to {c}\in {A}$
23 22 3ad2ant3 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {c}\in {A}$
24 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
25 24 3 4 hlatjcl
26 20 21 23 25 syl3anc
27 1 4 dalemqeb ${⊢}{\phi }\to {Q}\in {\mathrm{Base}}_{{K}}$
28 27 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {Q}\in {\mathrm{Base}}_{{K}}$
29 1 2 3 4 5 6 7 8 9 11 dalem29 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {H}\in {A}$
30 24 3 4 hlatjcl
31 20 29 23 30 syl3anc
32 24 2 3 latjlej12
33 16 18 26 28 31 32 syl122anc
34 13 14 33 mp2and
35 24 4 atbase ${⊢}{G}\in {A}\to {G}\in {\mathrm{Base}}_{{K}}$
36 21 35 syl ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {G}\in {\mathrm{Base}}_{{K}}$
37 24 4 atbase ${⊢}{H}\in {A}\to {H}\in {\mathrm{Base}}_{{K}}$
38 29 37 syl ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {H}\in {\mathrm{Base}}_{{K}}$
39 5 4 dalemcceb ${⊢}{\psi }\to {c}\in {\mathrm{Base}}_{{K}}$
40 39 3ad2ant3 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {c}\in {\mathrm{Base}}_{{K}}$
41 24 3 latjjdir
42 16 36 38 40 41 syl13anc
43 34 42 breqtrrd
44 1 2 3 4 5 6 7 8 9 12 dalem37
45 1 3 4 dalempjqeb
47 24 3 4 hlatjcl
48 20 21 29 47 syl3anc
49 24 3 latjcl
50 16 48 40 49 syl3anc
51 1 4 dalemreb ${⊢}{\phi }\to {R}\in {\mathrm{Base}}_{{K}}$
52 51 3ad2ant1 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {R}\in {\mathrm{Base}}_{{K}}$
53 1 2 3 4 5 6 7 8 9 12 dalem34 ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {I}\in {A}$
54 24 3 4 hlatjcl
55 20 53 23 54 syl3anc
56 24 2 3 latjlej12
57 16 46 50 52 55 56 syl122anc
58 43 44 57 mp2and
59 24 4 atbase ${⊢}{I}\in {A}\to {I}\in {\mathrm{Base}}_{{K}}$
60 53 59 syl ${⊢}\left({\phi }\wedge {Y}={Z}\wedge {\psi }\right)\to {I}\in {\mathrm{Base}}_{{K}}$
61 24 3 latjjdir
62 16 48 60 40 61 syl13anc
63 58 62 breqtrrd
64 8 63 eqbrtrid