Metamath Proof Explorer

Theorem dalem25

Description: Lemma for dath . Show that the dummy center of perspectivity c is different from auxiliary atom G . (Contributed by NM, 3-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
dalem23.m ⊢ ∧ ˙ = meet ⁡ K
dalem23.o ⊢ O = LPlanes ⁡ K
dalem23.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem23.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
dalem23.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
Assertion dalem25 ⊢ φ ∧ Y = Z ∧ ψ → c ≠ G

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 dalem23.m ⊢ ∧ ˙ = meet ⁡ K
7 dalem23.o ⊢ O = LPlanes ⁡ K
8 dalem23.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
9 dalem23.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
10 dalem23.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
11 1 2 3 4 dalemcnes ⊢ φ → C ≠ S
12 11 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → C ≠ S
13 5 dalemclccjdd ⊢ ψ → C ≤ ˙ c ∨ ˙ d
14 13 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → C ≤ ˙ c ∨ ˙ d
15 14 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ≤ ˙ c ∨ ˙ d
16 simpr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → c = G
17 1 dalemkelat ⊢ φ → K ∈ Lat
18 17 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ Lat
19 1 dalemkehl ⊢ φ → K ∈ HL
20 19 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
21 5 dalemccea ⊢ ψ → c ∈ A
22 21 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ A
23 1 dalempea ⊢ φ → P ∈ A
24 23 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → P ∈ A
25 eqid ⊢ Base K = Base K
26 25 3 4 hlatjcl ⊢ K ∈ HL ∧ c ∈ A ∧ P ∈ A → c ∨ ˙ P ∈ Base K
27 20 22 24 26 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ P ∈ Base K
28 5 dalemddea ⊢ ψ → d ∈ A
29 28 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → d ∈ A
30 1 dalemsea ⊢ φ → S ∈ A
31 30 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → S ∈ A
32 25 3 4 hlatjcl ⊢ K ∈ HL ∧ d ∈ A ∧ S ∈ A → d ∨ ˙ S ∈ Base K
33 20 29 31 32 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → d ∨ ˙ S ∈ Base K
34 25 2 6 latmle2 ⊢ K ∈ Lat ∧ c ∨ ˙ P ∈ Base K ∧ d ∨ ˙ S ∈ Base K → c ∨ ˙ P ∧ ˙ d ∨ ˙ S ≤ ˙ d ∨ ˙ S
35 18 27 33 34 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ P ∧ ˙ d ∨ ˙ S ≤ ˙ d ∨ ˙ S
36 10 35 eqbrtrid ⊢ φ ∧ Y = Z ∧ ψ → G ≤ ˙ d ∨ ˙ S
37 3 4 hlatjcom ⊢ K ∈ HL ∧ d ∈ A ∧ S ∈ A → d ∨ ˙ S = S ∨ ˙ d
38 20 29 31 37 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → d ∨ ˙ S = S ∨ ˙ d
39 36 38 breqtrd ⊢ φ ∧ Y = Z ∧ ψ → G ≤ ˙ S ∨ ˙ d
40 39 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → G ≤ ˙ S ∨ ˙ d
41 16 40 eqbrtrd ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → c ≤ ˙ S ∨ ˙ d
42 2 3 4 hlatlej2 ⊢ K ∈ HL ∧ S ∈ A ∧ d ∈ A → d ≤ ˙ S ∨ ˙ d
43 20 31 29 42 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → d ≤ ˙ S ∨ ˙ d
44 43 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → d ≤ ˙ S ∨ ˙ d
45 5 4 dalemcceb ⊢ ψ → c ∈ Base K
46 45 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ Base K
47 25 4 atbase ⊢ d ∈ A → d ∈ Base K
48 28 47 syl ⊢ ψ → d ∈ Base K
49 48 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → d ∈ Base K
50 25 3 4 hlatjcl ⊢ K ∈ HL ∧ S ∈ A ∧ d ∈ A → S ∨ ˙ d ∈ Base K
51 20 31 29 50 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → S ∨ ˙ d ∈ Base K
52 25 2 3 latjle12 ⊢ K ∈ Lat ∧ c ∈ Base K ∧ d ∈ Base K ∧ S ∨ ˙ d ∈ Base K → c ≤ ˙ S ∨ ˙ d ∧ d ≤ ˙ S ∨ ˙ d ↔ c ∨ ˙ d ≤ ˙ S ∨ ˙ d
53 18 46 49 51 52 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → c ≤ ˙ S ∨ ˙ d ∧ d ≤ ˙ S ∨ ˙ d ↔ c ∨ ˙ d ≤ ˙ S ∨ ˙ d
54 53 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → c ≤ ˙ S ∨ ˙ d ∧ d ≤ ˙ S ∨ ˙ d ↔ c ∨ ˙ d ≤ ˙ S ∨ ˙ d
55 41 44 54 mpbi2and ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → c ∨ ˙ d ≤ ˙ S ∨ ˙ d
56 1 4 dalemceb ⊢ φ → C ∈ Base K
57 56 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → C ∈ Base K
58 25 3 4 hlatjcl ⊢ K ∈ HL ∧ c ∈ A ∧ d ∈ A → c ∨ ˙ d ∈ Base K
59 20 22 29 58 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ d ∈ Base K
60 25 2 lattr ⊢ K ∈ Lat ∧ C ∈ Base K ∧ c ∨ ˙ d ∈ Base K ∧ S ∨ ˙ d ∈ Base K → C ≤ ˙ c ∨ ˙ d ∧ c ∨ ˙ d ≤ ˙ S ∨ ˙ d → C ≤ ˙ S ∨ ˙ d
61 18 57 59 51 60 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → C ≤ ˙ c ∨ ˙ d ∧ c ∨ ˙ d ≤ ˙ S ∨ ˙ d → C ≤ ˙ S ∨ ˙ d
62 61 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ≤ ˙ c ∨ ˙ d ∧ c ∨ ˙ d ≤ ˙ S ∨ ˙ d → C ≤ ˙ S ∨ ˙ d
63 15 55 62 mp2and ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ≤ ˙ S ∨ ˙ d
64 1 7 dalemyeb ⊢ φ → Y ∈ Base K
65 64 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → Y ∈ Base K
66 25 2 6 latmlem1 ⊢ K ∈ Lat ∧ C ∈ Base K ∧ S ∨ ˙ d ∈ Base K ∧ Y ∈ Base K → C ≤ ˙ S ∨ ˙ d → C ∧ ˙ Y ≤ ˙ S ∨ ˙ d ∧ ˙ Y
67 18 57 51 65 66 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → C ≤ ˙ S ∨ ˙ d → C ∧ ˙ Y ≤ ˙ S ∨ ˙ d ∧ ˙ Y
68 67 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ≤ ˙ S ∨ ˙ d → C ∧ ˙ Y ≤ ˙ S ∨ ˙ d ∧ ˙ Y
69 63 68 mpd ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ∧ ˙ Y ≤ ˙ S ∨ ˙ d ∧ ˙ Y
70 1 2 3 4 7 8 9 dalem17 ⊢ φ ∧ Y = Z → C ≤ ˙ Y
71 70 3adant3 ⊢ φ ∧ Y = Z ∧ ψ → C ≤ ˙ Y
72 25 2 6 latleeqm1 ⊢ K ∈ Lat ∧ C ∈ Base K ∧ Y ∈ Base K → C ≤ ˙ Y ↔ C ∧ ˙ Y = C
73 18 57 65 72 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → C ≤ ˙ Y ↔ C ∧ ˙ Y = C
74 71 73 mpbid ⊢ φ ∧ Y = Z ∧ ψ → C ∧ ˙ Y = C
75 74 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ∧ ˙ Y = C
76 1 2 3 4 9 dalemsly ⊢ φ ∧ Y = Z → S ≤ ˙ Y
77 76 3adant3 ⊢ φ ∧ Y = Z ∧ ψ → S ≤ ˙ Y
78 5 dalem-ddly ⊢ ψ → ¬ d ≤ ˙ Y
79 78 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → ¬ d ≤ ˙ Y
80 25 2 3 6 4 2atjm ⊢ K ∈ HL ∧ S ∈ A ∧ d ∈ A ∧ Y ∈ Base K ∧ S ≤ ˙ Y ∧ ¬ d ≤ ˙ Y → S ∨ ˙ d ∧ ˙ Y = S
81 20 31 29 65 77 79 80 syl132anc ⊢ φ ∧ Y = Z ∧ ψ → S ∨ ˙ d ∧ ˙ Y = S
82 81 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → S ∨ ˙ d ∧ ˙ Y = S
83 69 75 82 3brtr3d ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ≤ ˙ S
84 hlatl ⊢ K ∈ HL → K ∈ AtLat
85 19 84 syl ⊢ φ → K ∈ AtLat
86 1 2 3 4 7 8 dalemcea ⊢ φ → C ∈ A
87 2 4 atcmp ⊢ K ∈ AtLat ∧ C ∈ A ∧ S ∈ A → C ≤ ˙ S ↔ C = S
88 85 86 30 87 syl3anc ⊢ φ → C ≤ ˙ S ↔ C = S
89 88 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → C ≤ ˙ S ↔ C = S
90 89 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C ≤ ˙ S ↔ C = S
91 83 90 mpbid ⊢ φ ∧ Y = Z ∧ ψ ∧ c = G → C = S
92 91 ex ⊢ φ ∧ Y = Z ∧ ψ → c = G → C = S
93 92 necon3d ⊢ φ ∧ Y = Z ∧ ψ → C ≠ S → c ≠ G
94 12 93 mpd ⊢ φ ∧ Y = Z ∧ ψ → c ≠ G