Metamath Proof Explorer


Theorem dalem58

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

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 dalem58.m ˙=meetK
7 dalem58.o O=LPlanesK
8 dalem58.y Y=P˙Q˙R
9 dalem58.z Z=S˙T˙U
10 dalem58.e E=Q˙R˙T˙U
11 dalem58.g G=c˙P˙d˙S
12 dalem58.h H=c˙Q˙d˙T
13 dalem58.i I=c˙R˙d˙U
14 dalem58.b1 B=G˙H˙I˙Y
15 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
16 15 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
17 1 2 3 4 8 9 dalemrotyz φY=ZQ˙R˙P=T˙U˙S
18 17 3adant3 φY=ZψQ˙R˙P=T˙U˙S
19 1 2 3 4 5 8 dalemrotps φψcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
20 19 3adant2 φY=ZψcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
21 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
22 biid cAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙dcAdA¬c˙Q˙R˙Pdc¬d˙Q˙R˙PC˙c˙d
23 eqid Q˙R˙P=Q˙R˙P
24 eqid T˙U˙S=T˙U˙S
25 eqid H˙I˙G˙Q˙R˙P=H˙I˙G˙Q˙R˙P
26 21 2 3 4 22 6 7 23 24 10 12 13 11 25 dalem57 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˙dE˙H˙I˙G˙Q˙R˙P
27 16 18 20 26 syl3anc φY=ZψE˙H˙I˙G˙Q˙R˙P
28 1 dalemkehl φKHL
29 28 3ad2ant1 φY=ZψKHL
30 1 2 3 4 5 6 7 8 9 12 dalem29 φY=ZψHA
31 1 2 3 4 5 6 7 8 9 13 dalem34 φY=ZψIA
32 1 2 3 4 5 6 7 8 9 11 dalem23 φY=ZψGA
33 3 4 hlatjrot KHLHAIAGAH˙I˙G=G˙H˙I
34 29 30 31 32 33 syl13anc φY=ZψH˙I˙G=G˙H˙I
35 1 3 4 dalemqrprot φQ˙R˙P=P˙Q˙R
36 35 8 eqtr4di φQ˙R˙P=Y
37 36 3ad2ant1 φY=ZψQ˙R˙P=Y
38 34 37 oveq12d φY=ZψH˙I˙G˙Q˙R˙P=G˙H˙I˙Y
39 38 14 eqtr4di φY=ZψH˙I˙G˙Q˙R˙P=B
40 27 39 breqtrd φY=ZψE˙B