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 φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
dalem.l ˙ = K
dalem.j ˙ = join K
dalem.a A = Atoms K
dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
dalem44.m ˙ = meet K
dalem44.o O = LPlanes K
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 ψ K HL c A G A H A I A P A Q A R A G ˙ H ˙ I O Y O ¬ c ˙ G ˙ H ¬ c ˙ H ˙ I ¬ c ˙ I ˙ G ¬ c ˙ P ˙ Q ¬ c ˙ Q ˙ R ¬ c ˙ R ˙ P c ˙ G ˙ P c ˙ H ˙ Q c ˙ I ˙ R G ˙ H ˙ I Y

Proof

Step Hyp Ref Expression
1 dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
2 dalem.l ˙ = K
3 dalem.j ˙ = join K
4 dalem.a A = Atoms K
5 dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
6 dalem44.m ˙ = meet K
7 dalem44.o O = LPlanes K
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 φ K HL
14 13 3ad2ant1 φ Y = Z ψ K HL
15 5 dalemccea ψ c A
16 15 3ad2ant3 φ Y = Z ψ c A
17 14 16 jca φ Y = Z ψ K HL c A
18 1 2 3 4 5 6 7 8 9 10 dalem23 φ Y = Z ψ G A
19 1 2 3 4 5 6 7 8 9 11 dalem29 φ Y = Z ψ H A
20 1 2 3 4 5 6 7 8 9 12 dalem34 φ Y = Z ψ I A
21 18 19 20 3jca φ Y = Z ψ G A H A I A
22 1 dalempea φ P A
23 1 dalemqea φ Q A
24 1 dalemrea φ R A
25 22 23 24 3jca φ P A Q A R A
26 25 3ad2ant1 φ Y = Z ψ P A Q A R A
27 17 21 26 3jca φ Y = Z ψ K HL c A G A H A I A P A Q A R A
28 1 2 3 4 5 6 7 8 9 10 11 12 dalem42 φ Y = Z ψ G ˙ H ˙ I O
29 1 dalemyeo φ Y O
30 29 3ad2ant1 φ Y = Z ψ Y O
31 28 30 jca φ Y = Z ψ G ˙ H ˙ I O Y O
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 ˙ P c ˙ H ˙ Q c ˙ 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 ˙ P c ˙ G ˙ P c ˙ H ˙ Q c ˙ I ˙ R
46 27 31 45 3jca φ Y = Z ψ K HL c A G A H A I A P A Q A R A G ˙ H ˙ I O Y O ¬ c ˙ G ˙ H ¬ c ˙ H ˙ I ¬ c ˙ I ˙ G ¬ c ˙ P ˙ Q ¬ c ˙ Q ˙ R ¬ c ˙ R ˙ P c ˙ G ˙ P c ˙ H ˙ Q c ˙ I ˙ R
47 1 2 3 4 5 6 7 8 9 10 11 12 dalem43 φ Y = Z ψ G ˙ H ˙ I Y
48 46 47 jca φ Y = Z ψ K HL c A G A H A I A P A Q A R A G ˙ H ˙ I O Y O ¬ c ˙ G ˙ H ¬ c ˙ H ˙ I ¬ c ˙ I ˙ G ¬ c ˙ P ˙ Q ¬ c ˙ Q ˙ R ¬ c ˙ R ˙ P c ˙ G ˙ P c ˙ H ˙ Q c ˙ I ˙ R G ˙ H ˙ I Y