Metamath Proof Explorer


Theorem dalem14

Description: Lemma for dath . Planes Y and Z form a 3-dimensional space (when they are different). (Contributed by NM, 22-Jul-2012)

Ref Expression
Hypotheses dalema.ph φKHLCBaseKPAQARASATAUAYOZO¬C˙P˙Q¬C˙Q˙R¬C˙R˙P¬C˙S˙T¬C˙T˙U¬C˙U˙SC˙P˙SC˙Q˙TC˙R˙U
dalemc.l ˙=K
dalemc.j ˙=joinK
dalemc.a A=AtomsK
dalem14.o O=LPlanesK
dalem14.v V=LVolsK
dalem14.y Y=P˙Q˙R
dalem14.z Z=S˙T˙U
dalem14.w W=Y˙C
Assertion dalem14 φYZY˙ZV

Proof

Step Hyp Ref Expression
1 dalema.ph φKHLCBaseKPAQARASATAUAYOZO¬C˙P˙Q¬C˙Q˙R¬C˙R˙P¬C˙S˙T¬C˙T˙U¬C˙U˙SC˙P˙SC˙Q˙TC˙R˙U
2 dalemc.l ˙=K
3 dalemc.j ˙=joinK
4 dalemc.a A=AtomsK
5 dalem14.o O=LPlanesK
6 dalem14.v V=LVolsK
7 dalem14.y Y=P˙Q˙R
8 dalem14.z Z=S˙T˙U
9 dalem14.w W=Y˙C
10 1 2 3 4 5 7 8 9 dalem13 φYZY˙Z=W
11 1 2 3 4 5 6 7 8 9 dalem9 φYZWV
12 10 11 eqeltrd φYZY˙ZV