Metamath Proof Explorer


Theorem dalem36

Description: Lemma for dath . Analogue of dalem27 for I . (Contributed by NM, 8-Aug-2012)

Ref Expression
Hypotheses dalem.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
dalem.l ˙=K
dalem.j ˙=joinK
dalem.a A=AtomsK
dalem.ps ψcAdA¬c˙Ydc¬d˙YC˙c˙d
dalem34.m ˙=meetK
dalem34.o O=LPlanesK
dalem34.y Y=P˙Q˙R
dalem34.z Z=S˙T˙U
dalem34.i I=c˙R˙d˙U
Assertion dalem36 φY=Zψc˙I˙R

Proof

Step Hyp Ref Expression
1 dalem.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 dalem.l ˙=K
3 dalem.j ˙=joinK
4 dalem.a A=AtomsK
5 dalem.ps ψcAdA¬c˙Ydc¬d˙YC˙c˙d
6 dalem34.m ˙=meetK
7 dalem34.o O=LPlanesK
8 dalem34.y Y=P˙Q˙R
9 dalem34.z Z=S˙T˙U
10 dalem34.i I=c˙R˙d˙U
11 1 2 3 4 8 9 dalemrot φKHLCBaseKQARAPATAUASAQ˙R˙POT˙U˙SO¬C˙Q˙R¬C˙R˙P¬C˙P˙Q¬C˙T˙U¬C˙U˙S¬C˙S˙TC˙Q˙TC˙R˙UC˙P˙S
12 11 3ad2ant1 φY=ZψKHLCBaseKQARAPATAUASAQ˙R˙POT˙U˙SO¬C˙Q˙R¬C˙R˙P¬C˙P˙Q¬C˙T˙U¬C˙U˙S¬C˙S˙TC˙Q˙TC˙R˙UC˙P˙S
13 1 2 3 4 8 9 dalemrotyz φY=ZQ˙R˙P=T˙U˙S
14 13 3adant3 φY=ZψQ˙R˙P=T˙U˙S
15 1 2 3 4 5 8 dalemrotps φψcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
16 15 3adant2 φY=ZψcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
17 biid KHLCBaseKQARAPATAUASAQ˙R˙POT˙U˙SO¬C˙Q˙R¬C˙R˙P¬C˙P˙Q¬C˙T˙U¬C˙U˙S¬C˙S˙TC˙Q˙TC˙R˙UC˙P˙SKHLCBaseKQARAPATAUASAQ˙R˙POT˙U˙SO¬C˙Q˙R¬C˙R˙P¬C˙P˙Q¬C˙T˙U¬C˙U˙S¬C˙S˙TC˙Q˙TC˙R˙UC˙P˙S
18 biid cAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙dcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
19 eqid Q˙R˙P=Q˙R˙P
20 eqid T˙U˙S=T˙U˙S
21 17 2 3 4 18 6 7 19 20 10 dalem32 KHLCBaseKQARAPATAUASAQ˙R˙POT˙U˙SO¬C˙Q˙R¬C˙R˙P¬C˙P˙Q¬C˙T˙U¬C˙U˙S¬C˙S˙TC˙Q˙TC˙R˙UC˙P˙SQ˙R˙P=T˙U˙ScAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙dc˙I˙R
22 12 14 16 21 syl3anc φY=Zψc˙I˙R