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 ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑅 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑅 ) )