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 ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )