Metamath Proof Explorer

Theorem 3atlem4

Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)

Ref Expression
Hypotheses 3at.l ⊢ ≤ = ( le ‘ 𝐾 )
3at.j ⊢ ∨ = ( join ‘ 𝐾 )
3at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3atlem4 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 3at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 3at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 3at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝐾 ∈ HL )
5 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
6 simp13l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑆 ∈ 𝐴 )
7 simp13r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑇 ∈ 𝐴 )
8 simp123 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
9 6 7 8 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
10 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
11 4 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝐾 ∈ Lat )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
14 8 13 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 simp121 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
16 12 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
17 15 16 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
18 simp122 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
19 12 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
21 12 1 2 latnlej1l ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑅 ≠ 𝑃 )
22 11 14 17 20 10 21 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑅 ≠ 𝑃 )
23 22 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )
24 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑃 ≠ 𝑄 )
25 24 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → 𝑄 ≠ 𝑃 )
26 1 2 3 hlatexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑃 ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
27 4 18 8 15 25 26 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
28 10 27 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) )
29 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) )
30 1 2 3 3atlem3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑅 ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) )
31 4 5 9 10 23 28 29 30 syl331anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) ∧ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≠ 𝑄 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ≤ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑅 ) )