Metamath Proof Explorer


Theorem 4atexlemcnd

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) )
4thatlem0.l = ( le ‘ 𝐾 )
4thatlem0.j = ( join ‘ 𝐾 )
4thatlem0.m = ( meet ‘ 𝐾 )
4thatlem0.a 𝐴 = ( Atoms ‘ 𝐾 )
4thatlem0.h 𝐻 = ( LHyp ‘ 𝐾 )
4thatlem0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
4thatlem0.v 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
4thatlem0.c 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) )
4thatlem0.d 𝐷 = ( ( 𝑅 𝑇 ) ( 𝑃 𝑆 ) )
Assertion 4atexlemcnd ( 𝜑𝐶𝐷 )

Proof

Step Hyp Ref Expression
1 4thatlem.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) )
2 4thatlem0.l = ( le ‘ 𝐾 )
3 4thatlem0.j = ( join ‘ 𝐾 )
4 4thatlem0.m = ( meet ‘ 𝐾 )
5 4thatlem0.a 𝐴 = ( Atoms ‘ 𝐾 )
6 4thatlem0.h 𝐻 = ( LHyp ‘ 𝐾 )
7 4thatlem0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 4thatlem0.v 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
9 4thatlem0.c 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) )
10 4thatlem0.d 𝐷 = ( ( 𝑅 𝑇 ) ( 𝑃 𝑆 ) )
11 1 2 3 4 5 6 7 8 4atexlemtlw ( 𝜑𝑇 𝑊 )
12 1 2 3 4 5 6 7 8 9 4atexlemnclw ( 𝜑 → ¬ 𝐶 𝑊 )
13 nbrne2 ( ( 𝑇 𝑊 ∧ ¬ 𝐶 𝑊 ) → 𝑇𝐶 )
14 11 12 13 syl2anc ( 𝜑𝑇𝐶 )
15 1 4atexlemk ( 𝜑𝐾 ∈ HL )
16 1 4atexlemq ( 𝜑𝑄𝐴 )
17 1 4atexlemt ( 𝜑𝑇𝐴 )
18 3 5 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴 ) → ( 𝑄 𝑇 ) = ( 𝑇 𝑄 ) )
19 15 16 17 18 syl3anc ( 𝜑 → ( 𝑄 𝑇 ) = ( 𝑇 𝑄 ) )
20 simp221 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
21 1 20 sylbi ( 𝜑𝑅𝐴 )
22 3 5 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑇𝐴 ) → ( 𝑅 𝑇 ) = ( 𝑇 𝑅 ) )
23 15 21 17 22 syl3anc ( 𝜑 → ( 𝑅 𝑇 ) = ( 𝑇 𝑅 ) )
24 19 23 oveq12d ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) = ( ( 𝑇 𝑄 ) ( 𝑇 𝑅 ) ) )
25 1 4atexlemkc ( 𝜑𝐾 ∈ CvLat )
26 1 4atexlemp ( 𝜑𝑃𝐴 )
27 1 4atexlempnq ( 𝜑𝑃𝑄 )
28 simp223 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) )
29 1 28 sylbi ( 𝜑 → ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) )
30 5 3 cvlsupr6 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ) → 𝑅𝑄 )
31 30 necomd ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ) → 𝑄𝑅 )
32 25 26 16 21 27 29 31 syl132anc ( 𝜑𝑄𝑅 )
33 1 2 3 4 5 6 7 8 4atexlemntlpq ( 𝜑 → ¬ 𝑇 ( 𝑃 𝑄 ) )
34 5 3 cvlsupr7 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑅 𝑄 ) )
35 25 26 16 21 27 29 34 syl132anc ( 𝜑 → ( 𝑃 𝑄 ) = ( 𝑅 𝑄 ) )
36 3 5 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴 ) → ( 𝑄 𝑅 ) = ( 𝑅 𝑄 ) )
37 15 16 21 36 syl3anc ( 𝜑 → ( 𝑄 𝑅 ) = ( 𝑅 𝑄 ) )
38 35 37 eqtr4d ( 𝜑 → ( 𝑃 𝑄 ) = ( 𝑄 𝑅 ) )
39 38 breq2d ( 𝜑 → ( 𝑇 ( 𝑃 𝑄 ) ↔ 𝑇 ( 𝑄 𝑅 ) ) )
40 33 39 mtbid ( 𝜑 → ¬ 𝑇 ( 𝑄 𝑅 ) )
41 2 3 4 5 2llnma2 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑅𝐴𝑇𝐴 ) ∧ ( 𝑄𝑅 ∧ ¬ 𝑇 ( 𝑄 𝑅 ) ) ) → ( ( 𝑇 𝑄 ) ( 𝑇 𝑅 ) ) = 𝑇 )
42 15 16 21 17 32 40 41 syl132anc ( 𝜑 → ( ( 𝑇 𝑄 ) ( 𝑇 𝑅 ) ) = 𝑇 )
43 24 42 eqtr2d ( 𝜑𝑇 = ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) )
44 43 adantr ( ( 𝜑𝐶 = 𝐷 ) → 𝑇 = ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) )
45 1 4atexlemkl ( 𝜑𝐾 ∈ Lat )
46 1 3 5 4atexlemqtb ( 𝜑 → ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
47 1 3 5 4atexlempsb ( 𝜑 → ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
48 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
49 48 2 4 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑄 𝑇 ) )
50 45 46 47 49 syl3anc ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑄 𝑇 ) )
51 9 50 eqbrtrid ( 𝜑𝐶 ( 𝑄 𝑇 ) )
52 51 adantr ( ( 𝜑𝐶 = 𝐷 ) → 𝐶 ( 𝑄 𝑇 ) )
53 simpr ( ( 𝜑𝐶 = 𝐷 ) → 𝐶 = 𝐷 )
54 48 3 5 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑇𝐴 ) → ( 𝑅 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
55 15 21 17 54 syl3anc ( 𝜑 → ( 𝑅 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
56 48 2 4 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑅 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑅 𝑇 ) )
57 45 55 47 56 syl3anc ( 𝜑 → ( ( 𝑅 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑅 𝑇 ) )
58 10 57 eqbrtrid ( 𝜑𝐷 ( 𝑅 𝑇 ) )
59 58 adantr ( ( 𝜑𝐶 = 𝐷 ) → 𝐷 ( 𝑅 𝑇 ) )
60 53 59 eqbrtrd ( ( 𝜑𝐶 = 𝐷 ) → 𝐶 ( 𝑅 𝑇 ) )
61 1 2 3 4 5 6 7 8 9 4atexlemc ( 𝜑𝐶𝐴 )
62 48 5 atbase ( 𝐶𝐴𝐶 ∈ ( Base ‘ 𝐾 ) )
63 61 62 syl ( 𝜑𝐶 ∈ ( Base ‘ 𝐾 ) )
64 48 2 4 latlem12 ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑇 ) ) ↔ 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ) )
65 45 63 46 55 64 syl13anc ( 𝜑 → ( ( 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑇 ) ) ↔ 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ) )
66 65 adantr ( ( 𝜑𝐶 = 𝐷 ) → ( ( 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑇 ) ) ↔ 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ) )
67 52 60 66 mpbi2and ( ( 𝜑𝐶 = 𝐷 ) → 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) )
68 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
69 15 68 syl ( 𝜑𝐾 ∈ AtLat )
70 43 17 eqeltrrd ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ∈ 𝐴 )
71 2 5 atcmp ( ( 𝐾 ∈ AtLat ∧ 𝐶𝐴 ∧ ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ∈ 𝐴 ) → ( 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ↔ 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ) )
72 69 61 70 71 syl3anc ( 𝜑 → ( 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ↔ 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ) )
73 72 adantr ( ( 𝜑𝐶 = 𝐷 ) → ( 𝐶 ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ↔ 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) ) )
74 67 73 mpbid ( ( 𝜑𝐶 = 𝐷 ) → 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑅 𝑇 ) ) )
75 44 74 eqtr4d ( ( 𝜑𝐶 = 𝐷 ) → 𝑇 = 𝐶 )
76 75 ex ( 𝜑 → ( 𝐶 = 𝐷𝑇 = 𝐶 ) )
77 76 necon3d ( 𝜑 → ( 𝑇𝐶𝐶𝐷 ) )
78 14 77 mpd ( 𝜑𝐶𝐷 )