Metamath Proof Explorer


Theorem dalaw

Description: Desargues's law, derived from Desargues's theorem dath and with no conditions on the atoms. If triples <. P , Q , R >. and <. S , T , U >. are centrally perspective, i.e., ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) , then they are axially perspective. Theorem 13.3 of Crawley p. 110. (Contributed by NM, 7-Oct-2012)

Ref Expression
Hypotheses dalaw.l ˙=K
dalaw.j ˙=joinK
dalaw.m ˙=meetK
dalaw.a A=AtomsK
Assertion dalaw KHLPAQARASATAUAP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S

Proof

Step Hyp Ref Expression
1 dalaw.l ˙=K
2 dalaw.j ˙=joinK
3 dalaw.m ˙=meetK
4 dalaw.a A=AtomsK
5 eqid LPlanesK=LPlanesK
6 1 2 3 4 5 dalawlem14 KHL¬P˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
7 6 3expib KHL¬P˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
8 7 3exp KHL¬P˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
9 1 2 3 4 5 dalawlem15 KHL¬S˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
10 9 3expib KHL¬S˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
11 10 3exp KHL¬S˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
12 simp11 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAKHL
13 simp2 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAPAQARA
14 simp3 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUASATAUA
15 simp2ll KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙Q˙RLPlanesK
16 15 3ad2ant1 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙RLPlanesK
17 simp2rl KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙US˙T˙ULPlanesK
18 17 3ad2ant1 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAS˙T˙ULPlanesK
19 simp2lr KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙U¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P
20 19 3ad2ant1 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUA¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P
21 simp2rr KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙U¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙S
22 21 3ad2ant1 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUA¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙S
23 simp13 KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙S˙Q˙T˙R˙U
24 1 2 3 4 5 dalawlem1 KHLPAQARASATAUAP˙Q˙RLPlanesKS˙T˙ULPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
25 12 13 14 16 18 20 22 23 24 syl323anc KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
26 25 3expib KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
27 26 3exp KHLP˙Q˙RLPlanesK¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙PS˙T˙ULPlanesK¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
28 8 11 27 ecased KHLP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
29 28 exp4a KHLP˙S˙Q˙T˙R˙UPAQARASATAUAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
30 29 com34 KHLP˙S˙Q˙T˙R˙USATAUAPAQARAP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
31 30 com24 KHLPAQARASATAUAP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
32 31 3imp KHLPAQARASATAUAP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S