Metamath Proof Explorer


Theorem dalem1

Description: Lemma for dath . Show the lines P S and Q T are different. (Contributed by NM, 9-Aug-2012)

Ref Expression
Hypotheses dalema.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
dalemc.l ˙ = K
dalemc.j ˙ = join K
dalemc.a A = Atoms K
dalem1.o O = LPlanes K
dalem1.y Y = P ˙ Q ˙ R
Assertion dalem1 φ P ˙ S Q ˙ T

Proof

Step Hyp Ref Expression
1 dalema.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 dalemc.l ˙ = K
3 dalemc.j ˙ = join K
4 dalemc.a A = Atoms K
5 dalem1.o O = LPlanes K
6 dalem1.y Y = P ˙ Q ˙ R
7 1 dalemclpjs φ C ˙ P ˙ S
8 1 dalem-clpjq φ ¬ C ˙ P ˙ Q
9 8 adantr φ P ˙ S = Q ˙ T ¬ C ˙ P ˙ Q
10 1 dalemkehl φ K HL
11 1 dalempea φ P A
12 1 dalemsea φ S A
13 2 3 4 hlatlej1 K HL P A S A P ˙ P ˙ S
14 10 11 12 13 syl3anc φ P ˙ P ˙ S
15 14 adantr φ P ˙ S = Q ˙ T P ˙ P ˙ S
16 1 dalemqea φ Q A
17 1 dalemtea φ T A
18 2 3 4 hlatlej1 K HL Q A T A Q ˙ Q ˙ T
19 10 16 17 18 syl3anc φ Q ˙ Q ˙ T
20 19 adantr φ P ˙ S = Q ˙ T Q ˙ Q ˙ T
21 simpr φ P ˙ S = Q ˙ T P ˙ S = Q ˙ T
22 20 21 breqtrrd φ P ˙ S = Q ˙ T Q ˙ P ˙ S
23 1 dalemkelat φ K Lat
24 1 4 dalempeb φ P Base K
25 1 4 dalemqeb φ Q Base K
26 eqid Base K = Base K
27 26 3 4 hlatjcl K HL P A S A P ˙ S Base K
28 10 11 12 27 syl3anc φ P ˙ S Base K
29 26 2 3 latjle12 K Lat P Base K Q Base K P ˙ S Base K P ˙ P ˙ S Q ˙ P ˙ S P ˙ Q ˙ P ˙ S
30 23 24 25 28 29 syl13anc φ P ˙ P ˙ S Q ˙ P ˙ S P ˙ Q ˙ P ˙ S
31 30 adantr φ P ˙ S = Q ˙ T P ˙ P ˙ S Q ˙ P ˙ S P ˙ Q ˙ P ˙ S
32 15 22 31 mpbi2and φ P ˙ S = Q ˙ T P ˙ Q ˙ P ˙ S
33 1 dalemrea φ R A
34 1 dalemyeo φ Y O
35 3 4 5 6 lplnri1 K HL P A Q A R A Y O P Q
36 10 11 16 33 34 35 syl131anc φ P Q
37 2 3 4 ps-1 K HL P A Q A P Q P A S A P ˙ Q ˙ P ˙ S P ˙ Q = P ˙ S
38 10 11 16 36 11 12 37 syl132anc φ P ˙ Q ˙ P ˙ S P ˙ Q = P ˙ S
39 38 adantr φ P ˙ S = Q ˙ T P ˙ Q ˙ P ˙ S P ˙ Q = P ˙ S
40 32 39 mpbid φ P ˙ S = Q ˙ T P ˙ Q = P ˙ S
41 40 breq2d φ P ˙ S = Q ˙ T C ˙ P ˙ Q C ˙ P ˙ S
42 9 41 mtbid φ P ˙ S = Q ˙ T ¬ C ˙ P ˙ S
43 42 ex φ P ˙ S = Q ˙ T ¬ C ˙ P ˙ S
44 43 necon2ad φ C ˙ P ˙ S P ˙ S Q ˙ T
45 7 44 mpd φ P ˙ S Q ˙ T