Metamath Proof Explorer


Theorem dalem47

Description: Lemma for dath . Analogue of dalem45 for I G . (Contributed by NM, 16-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
dalem44.m ˙=meetK
dalem44.o O=LPlanesK
dalem44.y Y=P˙Q˙R
dalem44.z Z=S˙T˙U
dalem44.g G=c˙P˙d˙S
dalem44.h H=c˙Q˙d˙T
dalem44.i I=c˙R˙d˙U
Assertion dalem47 φY=Zψ¬c˙I˙G

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 dalem44.m ˙=meetK
7 dalem44.o O=LPlanesK
8 dalem44.y Y=P˙Q˙R
9 dalem44.z Z=S˙T˙U
10 dalem44.g G=c˙P˙d˙S
11 dalem44.h H=c˙Q˙d˙T
12 dalem44.i I=c˙R˙d˙U
13 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
14 13 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
15 1 2 3 4 8 9 dalemrotyz φY=ZQ˙R˙P=T˙U˙S
16 15 3adant3 φY=ZψQ˙R˙P=T˙U˙S
17 1 2 3 4 5 8 dalemrotps φψcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
18 17 3adant2 φY=ZψcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
19 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
20 biid cAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙dcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
21 eqid Q˙R˙P=Q˙R˙P
22 eqid T˙U˙S=T˙U˙S
23 19 2 3 4 20 6 7 21 22 11 12 10 dalem46 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˙d¬c˙I˙G
24 14 16 18 23 syl3anc φY=Zψ¬c˙I˙G