Metamath Proof Explorer


Theorem 3atlem3

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

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

Proof

Step Hyp Ref Expression
1 3at.l = ( le ‘ 𝐾 )
2 3at.j = ( join ‘ 𝐾 )
3 3at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) )
5 simpl21 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
6 simpl22 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → 𝑃𝑈 )
7 simpr ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → 𝑃 ( 𝑇 𝑈 ) )
8 6 7 jca ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → ( 𝑃𝑈𝑃 ( 𝑇 𝑈 ) ) )
9 simpl23 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → ¬ 𝑄 ( 𝑃 𝑈 ) )
10 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
11 1 2 3 3atlem2 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ( 𝑃𝑈𝑃 ( 𝑇 𝑈 ) ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )
12 4 5 8 9 10 11 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ 𝑃 ( 𝑇 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )
13 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) )
14 simpl21 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
15 simpr ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ¬ 𝑃 ( 𝑇 𝑈 ) )
16 simpl23 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ¬ 𝑄 ( 𝑃 𝑈 ) )
17 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
18 1 2 3 3atlem1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )
19 13 14 15 16 17 18 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )
20 12 19 pm2.61dan ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ 𝑃𝑈 ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )