Metamath Proof Explorer

Theorem 4atexlemunv

Description: Lemma for 4atexlem7 . (Contributed by NM, 21-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 ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
Assertion 4atexlemunv ( 𝜑 → 𝑈 ≠ 𝑉 )

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 1 4atexlemnslpq ⊢ ( 𝜑 → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
10 1 4atexlemk ⊢ ( 𝜑 → 𝐾 ∈ HL )
11 1 4atexlemp ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
12 1 4atexlems ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
13 2 3 5 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
14 10 11 12 13 syl3anc ⊢ ( 𝜑 → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
16 1 4atexlemkl ⊢ ( 𝜑 → 𝐾 ∈ Lat )
17 1 3 5 4atexlempsb ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18 1 6 4atexlemwb ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 2 4 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑆 ) )
21 16 17 18 20 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑆 ) )
22 8 21 eqbrtrid ⊢ ( 𝜑 → 𝑉 ≤ ( 𝑃 ∨ 𝑆 ) )
23 1 4atexlemkc ⊢ ( 𝜑 → 𝐾 ∈ CvLat )
24 1 2 3 4 5 6 7 8 4atexlemv ⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
25 19 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
26 16 17 18 25 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
27 8 26 eqbrtrid ⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
28 1 4atexlempw ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
29 28 simprd ⊢ ( 𝜑 → ¬ 𝑃 ≤ 𝑊 )
30 nbrne2 ⊢ ( ( 𝑉 ≤ 𝑊 ∧ ¬ 𝑃 ≤ 𝑊 ) → 𝑉 ≠ 𝑃 )
31 27 29 30 syl2anc ⊢ ( 𝜑 → 𝑉 ≠ 𝑃 )
32 2 3 5 cvlatexchb1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑉 ≠ 𝑃 ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑆 ) ) )
33 23 24 12 11 31 32 syl131anc ⊢ ( 𝜑 → ( 𝑉 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑆 ) ) )
34 22 33 mpbid ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑆 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑃 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑆 ) )
36 oveq2 ⊢ ( 𝑈 = 𝑉 → ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑉 ) )
37 36 eqcomd ⊢ ( 𝑈 = 𝑉 → ( 𝑃 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑈 ) )
38 1 4atexlemq ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
39 19 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
40 10 11 38 39 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
41 19 2 4 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) )
42 16 40 18 41 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑄 ) )
43 7 42 eqbrtrid ⊢ ( 𝜑 → 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) )
44 1 2 3 4 5 6 7 4atexlemu ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
45 19 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
46 16 40 18 45 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
47 7 46 eqbrtrid ⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
48 nbrne2 ⊢ ( ( 𝑈 ≤ 𝑊 ∧ ¬ 𝑃 ≤ 𝑊 ) → 𝑈 ≠ 𝑃 )
49 47 29 48 syl2anc ⊢ ( 𝜑 → 𝑈 ≠ 𝑃 )
50 2 3 5 cvlatexchb1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑈 ≠ 𝑃 ) → ( 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) ) )
51 23 44 38 11 49 50 syl131anc ⊢ ( 𝜑 → ( 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) ) )
52 43 51 mpbid ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) )
53 37 52 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑃 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) )
54 35 53 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑃 ∨ 𝑆 ) = ( 𝑃 ∨ 𝑄 ) )
55 15 54 breqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
56 55 ex ⊢ ( 𝜑 → ( 𝑈 = 𝑉 → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) )
57 56 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑈 ≠ 𝑉 ) )
58 9 57 mpd ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )