Metamath Proof Explorer

Theorem dalem44

Description: Lemma for dath . Dummy center of perspectivity c lies outside of plane G H I . (Contributed by NM, 16-Aug-2012)

Ref Expression
Hypotheses dalem.ph ⊢φ↔K∈HL∧C∈BaseK∧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 dalem44 ⊢φ∧Y=Z∧ψ→¬c≤˙G∨˙H∨˙I

Proof

Step Hyp Ref Expression
1 dalem.ph ⊢φ↔K∈HL∧C∈BaseK∧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 2 3 4 5 6 7 8 9 10 11 12 dalem43 ⊢φ∧Y=Z∧ψ→G∨˙H∨˙I≠Y
14 13 necomd ⊢φ∧Y=Z∧ψ→Y≠G∨˙H∨˙I
15 1 dalemkelat ⊢φ→K∈Lat
16 15 3ad2ant1 ⊢φ∧Y=Z∧ψ→K∈Lat
17 5 4 dalemcceb ⊢ψ→c∈BaseK
18 17 3ad2ant3 ⊢φ∧Y=Z∧ψ→c∈BaseK
19 1 2 3 4 5 6 7 8 9 10 11 12 dalem42 ⊢φ∧Y=Z∧ψ→G∨˙H∨˙I∈O
20 eqid ⊢BaseK=BaseK
21 20 7 lplnbase ⊢G∨˙H∨˙I∈O→G∨˙H∨˙I∈BaseK
22 19 21 syl ⊢φ∧Y=Z∧ψ→G∨˙H∨˙I∈BaseK
23 20 2 3 latleeqj1 ⊢K∈Lat∧c∈BaseK∧G∨˙H∨˙I∈BaseK→c≤˙G∨˙H∨˙I↔c∨˙G∨˙H∨˙I=G∨˙H∨˙I
24 16 18 22 23 syl3anc ⊢φ∧Y=Z∧ψ→c≤˙G∨˙H∨˙I↔c∨˙G∨˙H∨˙I=G∨˙H∨˙I
25 1 2 3 4 5 6 7 8 9 10 dalem28 ⊢φ∧Y=Z∧ψ→P≤˙G∨˙c
26 1 dalemkehl ⊢φ→K∈HL
27 26 3ad2ant1 ⊢φ∧Y=Z∧ψ→K∈HL
28 5 dalemccea ⊢ψ→c∈A
29 28 3ad2ant3 ⊢φ∧Y=Z∧ψ→c∈A
30 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢φ∧Y=Z∧ψ→G∈A
31 3 4 hlatjcom ⊢K∈HL∧c∈A∧G∈A→c∨˙G=G∨˙c
32 27 29 30 31 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙G=G∨˙c
33 25 32 breqtrrd ⊢φ∧Y=Z∧ψ→P≤˙c∨˙G
34 1 2 3 4 5 6 7 8 9 11 dalem33 ⊢φ∧Y=Z∧ψ→Q≤˙H∨˙c
35 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢φ∧Y=Z∧ψ→H∈A
36 3 4 hlatjcom ⊢K∈HL∧c∈A∧H∈A→c∨˙H=H∨˙c
37 27 29 35 36 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙H=H∨˙c
38 34 37 breqtrrd ⊢φ∧Y=Z∧ψ→Q≤˙c∨˙H
39 1 4 dalempeb ⊢φ→P∈BaseK
40 39 3ad2ant1 ⊢φ∧Y=Z∧ψ→P∈BaseK
41 20 3 4 hlatjcl ⊢K∈HL∧c∈A∧G∈A→c∨˙G∈BaseK
42 27 29 30 41 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙G∈BaseK
43 1 4 dalemqeb ⊢φ→Q∈BaseK
44 43 3ad2ant1 ⊢φ∧Y=Z∧ψ→Q∈BaseK
45 20 3 4 hlatjcl ⊢K∈HL∧c∈A∧H∈A→c∨˙H∈BaseK
46 27 29 35 45 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙H∈BaseK
47 20 2 3 latjlej12 ⊢K∈Lat∧P∈BaseK∧c∨˙G∈BaseK∧Q∈BaseK∧c∨˙H∈BaseK→P≤˙c∨˙G∧Q≤˙c∨˙H→P∨˙Q≤˙c∨˙G∨˙c∨˙H
48 16 40 42 44 46 47 syl122anc ⊢φ∧Y=Z∧ψ→P≤˙c∨˙G∧Q≤˙c∨˙H→P∨˙Q≤˙c∨˙G∨˙c∨˙H
49 33 38 48 mp2and ⊢φ∧Y=Z∧ψ→P∨˙Q≤˙c∨˙G∨˙c∨˙H
50 20 4 atbase ⊢G∈A→G∈BaseK
51 30 50 syl ⊢φ∧Y=Z∧ψ→G∈BaseK
52 20 4 atbase ⊢H∈A→H∈BaseK
53 35 52 syl ⊢φ∧Y=Z∧ψ→H∈BaseK
54 20 3 latjjdi ⊢K∈Lat∧c∈BaseK∧G∈BaseK∧H∈BaseK→c∨˙G∨˙H=c∨˙G∨˙c∨˙H
55 16 18 51 53 54 syl13anc ⊢φ∧Y=Z∧ψ→c∨˙G∨˙H=c∨˙G∨˙c∨˙H
56 49 55 breqtrrd ⊢φ∧Y=Z∧ψ→P∨˙Q≤˙c∨˙G∨˙H
57 1 2 3 4 5 6 7 8 9 12 dalem37 ⊢φ∧Y=Z∧ψ→R≤˙I∨˙c
58 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢φ∧Y=Z∧ψ→I∈A
59 3 4 hlatjcom ⊢K∈HL∧c∈A∧I∈A→c∨˙I=I∨˙c
60 27 29 58 59 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙I=I∨˙c
61 57 60 breqtrrd ⊢φ∧Y=Z∧ψ→R≤˙c∨˙I
62 1 3 4 dalempjqeb ⊢φ→P∨˙Q∈BaseK
63 62 3ad2ant1 ⊢φ∧Y=Z∧ψ→P∨˙Q∈BaseK
64 20 3 4 hlatjcl ⊢K∈HL∧G∈A∧H∈A→G∨˙H∈BaseK
65 27 30 35 64 syl3anc ⊢φ∧Y=Z∧ψ→G∨˙H∈BaseK
66 20 3 latjcl ⊢K∈Lat∧c∈BaseK∧G∨˙H∈BaseK→c∨˙G∨˙H∈BaseK
67 16 18 65 66 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙G∨˙H∈BaseK
68 1 4 dalemreb ⊢φ→R∈BaseK
69 68 3ad2ant1 ⊢φ∧Y=Z∧ψ→R∈BaseK
70 20 3 4 hlatjcl ⊢K∈HL∧c∈A∧I∈A→c∨˙I∈BaseK
71 27 29 58 70 syl3anc ⊢φ∧Y=Z∧ψ→c∨˙I∈BaseK
72 20 2 3 latjlej12 ⊢K∈Lat∧P∨˙Q∈BaseK∧c∨˙G∨˙H∈BaseK∧R∈BaseK∧c∨˙I∈BaseK→P∨˙Q≤˙c∨˙G∨˙H∧R≤˙c∨˙I→P∨˙Q∨˙R≤˙c∨˙G∨˙H∨˙c∨˙I
73 16 63 67 69 71 72 syl122anc ⊢φ∧Y=Z∧ψ→P∨˙Q≤˙c∨˙G∨˙H∧R≤˙c∨˙I→P∨˙Q∨˙R≤˙c∨˙G∨˙H∨˙c∨˙I
74 56 61 73 mp2and ⊢φ∧Y=Z∧ψ→P∨˙Q∨˙R≤˙c∨˙G∨˙H∨˙c∨˙I
75 20 4 atbase ⊢I∈A→I∈BaseK
76 58 75 syl ⊢φ∧Y=Z∧ψ→I∈BaseK
77 20 3 latjjdi ⊢K∈Lat∧c∈BaseK∧G∨˙H∈BaseK∧I∈BaseK→c∨˙G∨˙H∨˙I=c∨˙G∨˙H∨˙c∨˙I
78 16 18 65 76 77 syl13anc ⊢φ∧Y=Z∧ψ→c∨˙G∨˙H∨˙I=c∨˙G∨˙H∨˙c∨˙I
79 74 78 breqtrrd ⊢φ∧Y=Z∧ψ→P∨˙Q∨˙R≤˙c∨˙G∨˙H∨˙I
80 8 79 eqbrtrid ⊢φ∧Y=Z∧ψ→Y≤˙c∨˙G∨˙H∨˙I
81 breq2 ⊢c∨˙G∨˙H∨˙I=G∨˙H∨˙I→Y≤˙c∨˙G∨˙H∨˙I↔Y≤˙G∨˙H∨˙I
82 80 81 syl5ibcom ⊢φ∧Y=Z∧ψ→c∨˙G∨˙H∨˙I=G∨˙H∨˙I→Y≤˙G∨˙H∨˙I
83 24 82 sylbid ⊢φ∧Y=Z∧ψ→c≤˙G∨˙H∨˙I→Y≤˙G∨˙H∨˙I
84 1 dalemyeo ⊢φ→Y∈O
85 84 3ad2ant1 ⊢φ∧Y=Z∧ψ→Y∈O
86 2 7 lplncmp ⊢K∈HL∧Y∈O∧G∨˙H∨˙I∈O→Y≤˙G∨˙H∨˙I↔Y=G∨˙H∨˙I
87 27 85 19 86 syl3anc ⊢φ∧Y=Z∧ψ→Y≤˙G∨˙H∨˙I↔Y=G∨˙H∨˙I
88 83 87 sylibd ⊢φ∧Y=Z∧ψ→c≤˙G∨˙H∨˙I→Y=G∨˙H∨˙I
89 88 necon3ad ⊢φ∧Y=Z∧ψ→Y≠G∨˙H∨˙I→¬c≤˙G∨˙H∨˙I
90 14 89 mpd ⊢φ∧Y=Z∧ψ→¬c≤˙G∨˙H∨˙I