Metamath Proof Explorer


Theorem dalem51

Description: Lemma for dath . Construct the condition ph with c , G H I , and Y in place of C , Y , and Z respectively. This lets us reuse the special case of Desargues's theorem where Y =/= Z , to eventually prove the case where Y = Z . (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 dalem51 φY=ZψKHLcAGAHAIAPAQARAG˙H˙IOYO¬c˙G˙H¬c˙H˙I¬c˙I˙G¬c˙P˙Q¬c˙Q˙R¬c˙R˙Pc˙G˙Pc˙H˙Qc˙I˙RG˙H˙IY

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 dalemkehl φKHL
14 13 3ad2ant1 φY=ZψKHL
15 5 dalemccea ψcA
16 15 3ad2ant3 φY=ZψcA
17 14 16 jca φY=ZψKHLcA
18 1 2 3 4 5 6 7 8 9 10 dalem23 φY=ZψGA
19 1 2 3 4 5 6 7 8 9 11 dalem29 φY=ZψHA
20 1 2 3 4 5 6 7 8 9 12 dalem34 φY=ZψIA
21 18 19 20 3jca φY=ZψGAHAIA
22 1 dalempea φPA
23 1 dalemqea φQA
24 1 dalemrea φRA
25 22 23 24 3jca φPAQARA
26 25 3ad2ant1 φY=ZψPAQARA
27 17 21 26 3jca φY=ZψKHLcAGAHAIAPAQARA
28 1 2 3 4 5 6 7 8 9 10 11 12 dalem42 φY=ZψG˙H˙IO
29 1 dalemyeo φYO
30 29 3ad2ant1 φY=ZψYO
31 28 30 jca φY=ZψG˙H˙IOYO
32 1 2 3 4 5 6 7 8 9 10 11 12 dalem45 φY=Zψ¬c˙G˙H
33 1 2 3 4 5 6 7 8 9 10 11 12 dalem46 φY=Zψ¬c˙H˙I
34 1 2 3 4 5 6 7 8 9 10 11 12 dalem47 φY=Zψ¬c˙I˙G
35 32 33 34 3jca φY=Zψ¬c˙G˙H¬c˙H˙I¬c˙I˙G
36 1 2 3 4 5 6 7 8 9 10 11 12 dalem48 φψ¬c˙P˙Q
37 1 2 3 4 5 6 7 8 9 10 11 12 dalem49 φψ¬c˙Q˙R
38 1 2 3 4 5 6 7 8 9 10 11 12 dalem50 φψ¬c˙R˙P
39 36 37 38 3jca φψ¬c˙P˙Q¬c˙Q˙R¬c˙R˙P
40 39 3adant2 φY=Zψ¬c˙P˙Q¬c˙Q˙R¬c˙R˙P
41 1 2 3 4 5 6 7 8 9 10 dalem27 φY=Zψc˙G˙P
42 1 2 3 4 5 6 7 8 9 11 dalem32 φY=Zψc˙H˙Q
43 1 2 3 4 5 6 7 8 9 12 dalem36 φY=Zψc˙I˙R
44 41 42 43 3jca φY=Zψc˙G˙Pc˙H˙Qc˙I˙R
45 35 40 44 3jca φY=Zψ¬c˙G˙H¬c˙H˙I¬c˙I˙G¬c˙P˙Q¬c˙Q˙R¬c˙R˙Pc˙G˙Pc˙H˙Qc˙I˙R
46 27 31 45 3jca φY=ZψKHLcAGAHAIAPAQARAG˙H˙IOYO¬c˙G˙H¬c˙H˙I¬c˙I˙G¬c˙P˙Q¬c˙Q˙R¬c˙R˙Pc˙G˙Pc˙H˙Qc˙I˙R
47 1 2 3 4 5 6 7 8 9 10 11 12 dalem43 φY=ZψG˙H˙IY
48 46 47 jca φY=ZψKHLcAGAHAIAPAQARAG˙H˙IOYO¬c˙G˙H¬c˙H˙I¬c˙I˙G¬c˙P˙Q¬c˙Q˙R¬c˙R˙Pc˙G˙Pc˙H˙Qc˙I˙RG˙H˙IY