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 ˙ = join K
dalaw.m ˙ = meet K
dalaw.a A = Atoms K
Assertion dalaw K HL P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S

Proof

Step Hyp Ref Expression
1 dalaw.l ˙ = K
2 dalaw.j ˙ = join K
3 dalaw.m ˙ = meet K
4 dalaw.a A = Atoms K
5 eqid LPlanes K = LPlanes K
6 1 2 3 4 5 dalawlem14 K HL ¬ P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
7 6 3expib K HL ¬ P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
8 7 3exp K HL ¬ P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
9 1 2 3 4 5 dalawlem15 K HL ¬ S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
10 9 3expib K HL ¬ S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
11 10 3exp K HL ¬ S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
12 simp11 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K HL
13 simp2 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A Q A R A
14 simp3 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S A T A U A
15 simp2ll K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P ˙ Q ˙ R LPlanes K
16 15 3ad2ant1 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ R LPlanes K
17 simp2rl K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U S ˙ T ˙ U LPlanes K
18 17 3ad2ant1 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ T ˙ U LPlanes K
19 simp2lr K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ 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 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P
21 simp2rr K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ 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 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S
23 simp13 K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U
24 1 2 3 4 5 dalawlem1 K HL P A Q A R A S A T A U A P ˙ Q ˙ R LPlanes K S ˙ T ˙ U LPlanes K ¬ 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 ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
25 12 13 14 16 18 20 22 23 24 syl323anc K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
26 25 3expib K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
27 26 3exp K HL P ˙ Q ˙ R LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P S ˙ T ˙ U LPlanes K ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
28 8 11 27 ecased K HL P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
29 28 exp4a K HL P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
30 29 com34 K HL P ˙ S ˙ Q ˙ T ˙ R ˙ U S A T A U A P A Q A R A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
31 30 com24 K HL P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
32 31 3imp K HL P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S