# Metamath Proof Explorer

## Theorem dalem8

Description: Lemma for dath . Plane Z belongs to the 3-dimensional space. (Contributed by NM, 21-Jul-2012)

Ref Expression
Hypotheses dalema.ph
dalemc.l
dalemc.j
dalemc.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dalem6.o ${⊢}{O}=\mathrm{LPlanes}\left({K}\right)$
dalem6.y
dalem6.z
dalem6.w
Assertion dalem8

### Proof

Step Hyp Ref Expression
1 dalema.ph
2 dalemc.l
3 dalemc.j
4 dalemc.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 dalem6.o ${⊢}{O}=\mathrm{LPlanes}\left({K}\right)$
6 dalem6.y
7 dalem6.z
8 dalem6.w
9 1 2 3 4 5 6 7 8 dalem6
10 1 2 3 4 5 6 7 8 dalem7
11 1 dalemkelat ${⊢}{\phi }\to {K}\in \mathrm{Lat}$
12 1 4 dalemseb ${⊢}{\phi }\to {S}\in {\mathrm{Base}}_{{K}}$
13 1 4 dalemteb ${⊢}{\phi }\to {T}\in {\mathrm{Base}}_{{K}}$
14 1 5 dalemyeb ${⊢}{\phi }\to {Y}\in {\mathrm{Base}}_{{K}}$
15 1 4 dalemceb ${⊢}{\phi }\to {C}\in {\mathrm{Base}}_{{K}}$
16 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
17 16 3 latjcl
18 11 14 15 17 syl3anc
19 8 18 eqeltrid ${⊢}{\phi }\to {W}\in {\mathrm{Base}}_{{K}}$
20 16 2 3 latjle12
21 11 12 13 19 20 syl13anc
22 9 10 21 mpbi2and
23 1 2 3 4 5 6 8 dalem5
24 1 3 4 dalemsjteb
25 1 4 dalemueb ${⊢}{\phi }\to {U}\in {\mathrm{Base}}_{{K}}$
26 16 2 3 latjle12
27 11 24 25 19 26 syl13anc
28 22 23 27 mpbi2and
29 7 28 eqbrtrid