Metamath Proof Explorer

Theorem 4atexlemswapqr

Description: Lemma for 4atexlem7 . Swap Q and R , so that theorems involving C can be reused for D . Note that U must be expanded because it involves Q . (Contributed by NM, 25-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
4thatlemslps.l ⊢ ≤ = ( le ‘ 𝐾 )
4thatlemslps.j ⊢ ∨ = ( join ‘ 𝐾 )
4thatlemslps.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4thatlemsw.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion 4atexlemswapqr ( 𝜑 → ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 4thatlem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
2 4thatlemslps.l ⊢ ≤ = ( le ‘ 𝐾 )
3 4thatlemslps.j ⊢ ∨ = ( join ‘ 𝐾 )
4 4thatlemslps.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 4thatlemsw.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
6 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 1 6 sylbi ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 1 4atexlempw ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
9 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) )
10 3simpa ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
11 9 10 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
12 1 11 sylbi ⊢ ( 𝜑 → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
13 7 8 12 3jca ⊢ ( 𝜑 → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) )
14 1 4atexlems ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
15 1 4atexlemq ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
16 simp13r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑄 ≤ 𝑊 )
17 1 16 sylbi ⊢ ( 𝜑 → ¬ 𝑄 ≤ 𝑊 )
18 1 4atexlemkc ⊢ ( 𝜑 → 𝐾 ∈ CvLat )
19 1 4atexlemp ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
20 12 simpld ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
21 1 4atexlempnq ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
22 simp223 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
23 1 22 sylbi ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
24 4 3 cvlsupr7 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑄 ) )
25 18 19 15 20 21 23 24 syl132anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑄 ) )
26 15 17 25 3jca ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑄 ) ) )
27 1 4atexlemt ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
28 4 3 cvlsupr8 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) )
29 18 19 15 20 21 23 28 syl132anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) )
30 29 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) )
31 5 30 syl5eq ⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) )
32 31 oveq1d ⊢ ( 𝜑 → ( 𝑈 ∨ 𝑇 ) = ( ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∨ 𝑇 ) )
33 1 4atexlemutvt ⊢ ( 𝜑 → ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) )
34 32 33 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) )
35 27 34 jca ⊢ ( 𝜑 → ( 𝑇 ∈ 𝐴 ∧ ( ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) )
36 14 26 35 3jca ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐴 ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) )
37 4 3 cvlsupr5 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ≠ 𝑃 )
38 37 necomd ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ≠ 𝑅 )
39 18 19 15 20 21 23 38 syl132anc ⊢ ( 𝜑 → 𝑃 ≠ 𝑅 )
40 1 4atexlemnslpq ⊢ ( 𝜑 → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
41 29 eqcomd ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) )
42 41 breq2d ⊢ ( 𝜑 → ( 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ↔ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) )
43 40 42 mtbird ⊢ ( 𝜑 → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) )
44 39 43 jca ⊢ ( 𝜑 → ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ) )
45 13 36 44 3jca ⊢ ( 𝜑 → ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑄 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑅 ) ) ) )