Metamath Proof Explorer


Theorem dalem54

Description: Lemma for dath . Line G H intersects the auxiliary axis of perspectivity B . (Contributed by NM, 8-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
dalem54.m ˙ = meet K
dalem54.o O = LPlanes K
dalem54.y Y = P ˙ Q ˙ R
dalem54.z Z = S ˙ T ˙ U
dalem54.g G = c ˙ P ˙ d ˙ S
dalem54.h H = c ˙ Q ˙ d ˙ T
dalem54.i I = c ˙ R ˙ d ˙ U
dalem54.b1 B = G ˙ H ˙ I ˙ Y
Assertion dalem54 φ Y = Z ψ G ˙ H ˙ B A

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 dalem54.m ˙ = meet K
7 dalem54.o O = LPlanes K
8 dalem54.y Y = P ˙ Q ˙ R
9 dalem54.z Z = S ˙ T ˙ U
10 dalem54.g G = c ˙ P ˙ d ˙ S
11 dalem54.h H = c ˙ Q ˙ d ˙ T
12 dalem54.i I = c ˙ R ˙ d ˙ U
13 dalem54.b1 B = G ˙ H ˙ I ˙ Y
14 1 dalemkehl φ K HL
15 14 3ad2ant1 φ Y = Z ψ K HL
16 1 2 3 4 5 6 7 8 9 10 dalem23 φ Y = Z ψ G A
17 1 2 3 4 5 6 7 8 9 11 dalem29 φ Y = Z ψ H A
18 1 2 3 4 5 6 7 8 9 10 11 12 dalem41 φ Y = Z ψ G H
19 eqid LLines K = LLines K
20 3 4 19 llni2 K HL G A H A G H G ˙ H LLines K
21 15 16 17 18 20 syl31anc φ Y = Z ψ G ˙ H LLines K
22 1 2 3 4 5 6 19 7 8 9 10 11 12 13 dalem53 φ Y = Z ψ B LLines K
23 1 dalemkelat φ K Lat
24 23 3ad2ant1 φ Y = Z ψ K Lat
25 eqid Base K = Base K
26 25 19 llnbase G ˙ H LLines K G ˙ H Base K
27 21 26 syl φ Y = Z ψ G ˙ H Base K
28 1 2 3 4 5 6 7 8 9 12 dalem34 φ Y = Z ψ I A
29 25 4 atbase I A I Base K
30 28 29 syl φ Y = Z ψ I Base K
31 25 3 latjcl K Lat G ˙ H Base K I Base K G ˙ H ˙ I Base K
32 24 27 30 31 syl3anc φ Y = Z ψ G ˙ H ˙ I Base K
33 1 7 dalemyeb φ Y Base K
34 33 3ad2ant1 φ Y = Z ψ Y Base K
35 25 2 6 latmle2 K Lat G ˙ H ˙ I Base K Y Base K G ˙ H ˙ I ˙ Y ˙ Y
36 24 32 34 35 syl3anc φ Y = Z ψ G ˙ H ˙ I ˙ Y ˙ Y
37 13 36 eqbrtrid φ Y = Z ψ B ˙ Y
38 1 2 3 4 5 6 7 8 9 10 dalem24 φ Y = Z ψ ¬ G ˙ Y
39 25 4 atbase G A G Base K
40 16 39 syl φ Y = Z ψ G Base K
41 25 4 atbase H A H Base K
42 17 41 syl φ Y = Z ψ H Base K
43 25 2 3 latjle12 K Lat G Base K H Base K Y Base K G ˙ Y H ˙ Y G ˙ H ˙ Y
44 24 40 42 34 43 syl13anc φ Y = Z ψ G ˙ Y H ˙ Y G ˙ H ˙ Y
45 simpl G ˙ Y H ˙ Y G ˙ Y
46 44 45 syl6bir φ Y = Z ψ G ˙ H ˙ Y G ˙ Y
47 38 46 mtod φ Y = Z ψ ¬ G ˙ H ˙ Y
48 nbrne2 B ˙ Y ¬ G ˙ H ˙ Y B G ˙ H
49 37 47 48 syl2anc φ Y = Z ψ B G ˙ H
50 49 necomd φ Y = Z ψ G ˙ H B
51 hlatl K HL K AtLat
52 15 51 syl φ Y = Z ψ K AtLat
53 25 19 llnbase B LLines K B Base K
54 22 53 syl φ Y = Z ψ B Base K
55 25 6 latmcl K Lat G ˙ H Base K B Base K G ˙ H ˙ B Base K
56 24 27 54 55 syl3anc φ Y = Z ψ G ˙ H ˙ B Base K
57 1 2 3 4 5 6 7 8 9 10 11 12 dalem52 φ Y = Z ψ G ˙ H ˙ P ˙ Q A
58 1 3 4 dalempjqeb φ P ˙ Q Base K
59 58 3ad2ant1 φ Y = Z ψ P ˙ Q Base K
60 25 2 6 latmle1 K Lat G ˙ H Base K P ˙ Q Base K G ˙ H ˙ P ˙ Q ˙ G ˙ H
61 24 27 59 60 syl3anc φ Y = Z ψ G ˙ H ˙ P ˙ Q ˙ G ˙ H
62 1 2 3 4 5 6 7 8 9 10 11 12 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
63 62 simpld φ 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
64 25 4 atbase c A c Base K
65 64 anim2i K HL c A K HL c Base K
66 65 3anim1i K HL c A G A H A I A P A Q A R A K HL c Base K G A H A I A P A Q A R A
67 biid K HL c Base K 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 K HL c Base K 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
68 eqid G ˙ H ˙ I = G ˙ H ˙ I
69 eqid G ˙ H ˙ P ˙ Q = G ˙ H ˙ P ˙ Q
70 67 2 3 4 6 7 68 8 13 69 dalem10 K HL c Base K 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 ˙ P ˙ Q ˙ B
71 66 70 syl3an1 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 ˙ P ˙ Q ˙ B
72 63 71 syl φ Y = Z ψ G ˙ H ˙ P ˙ Q ˙ B
73 25 6 latmcl K Lat G ˙ H Base K P ˙ Q Base K G ˙ H ˙ P ˙ Q Base K
74 24 27 59 73 syl3anc φ Y = Z ψ G ˙ H ˙ P ˙ Q Base K
75 25 2 6 latlem12 K Lat G ˙ H ˙ P ˙ Q Base K G ˙ H Base K B Base K G ˙ H ˙ P ˙ Q ˙ G ˙ H G ˙ H ˙ P ˙ Q ˙ B G ˙ H ˙ P ˙ Q ˙ G ˙ H ˙ B
76 24 74 27 54 75 syl13anc φ Y = Z ψ G ˙ H ˙ P ˙ Q ˙ G ˙ H G ˙ H ˙ P ˙ Q ˙ B G ˙ H ˙ P ˙ Q ˙ G ˙ H ˙ B
77 61 72 76 mpbi2and φ Y = Z ψ G ˙ H ˙ P ˙ Q ˙ G ˙ H ˙ B
78 eqid 0. K = 0. K
79 25 2 78 4 atlen0 K AtLat G ˙ H ˙ B Base K G ˙ H ˙ P ˙ Q A G ˙ H ˙ P ˙ Q ˙ G ˙ H ˙ B G ˙ H ˙ B 0. K
80 52 56 57 77 79 syl31anc φ Y = Z ψ G ˙ H ˙ B 0. K
81 6 78 4 19 2llnmat K HL G ˙ H LLines K B LLines K G ˙ H B G ˙ H ˙ B 0. K G ˙ H ˙ B A
82 15 21 22 50 80 81 syl32anc φ Y = Z ψ G ˙ H ˙ B A