Metamath Proof Explorer


Theorem 4atlem12b

Description: Lemma for 4at . Substitute T for P (cont.). (Contributed by NM, 11-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 4at.l = ( le ‘ 𝐾 )
2 4at.j = ( join ‘ 𝐾 )
3 4at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) )
5 simp121 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑅𝐴 )
6 simp122 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑆𝐴 )
7 5 6 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑅𝐴𝑆𝐴 ) )
8 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) )
9 4 7 8 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) )
10 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
11 9 10 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) )
12 simp3lr ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
13 simp3rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
14 simp3rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
15 simp111 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝐾 ∈ HL )
16 15 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝐾 ∈ Lat )
17 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18 17 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
19 5 18 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
20 17 3 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
21 6 20 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
22 simp123 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑇𝐴 )
23 simp131 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑈𝐴 )
24 17 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴 ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
25 15 22 23 24 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
26 simp132 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑉𝐴 )
27 simp133 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑊𝐴 )
28 17 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑉𝐴𝑊𝐴 ) → ( 𝑉 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
29 15 26 27 28 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑉 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
30 17 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑉 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
31 16 25 29 30 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
32 17 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ↔ ( 𝑅 𝑆 ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
33 16 19 21 31 32 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ↔ ( 𝑅 𝑆 ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
34 13 14 33 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑅 𝑆 ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
35 simp113 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑄𝐴 )
36 17 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
37 35 36 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
38 17 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
39 15 5 6 38 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
40 17 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ ( 𝑅 𝑆 ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ↔ ( 𝑄 ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
41 16 37 39 31 40 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ ( 𝑅 𝑆 ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ↔ ( 𝑄 ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
42 12 34 41 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑄 ( 𝑅 𝑆 ) ) ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
43 simp3ll ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
44 simp112 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → 𝑃𝐴 )
45 simp2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) )
46 1 2 3 4atlem12a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
47 15 44 22 8 45 46 syl311anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )
48 43 47 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )
49 42 48 breqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( 𝑄 ( 𝑅 𝑆 ) ) ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) )
50 1 2 3 4atlem11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( 𝑄 ( 𝑅 𝑆 ) ) ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) ) )
51 11 49 50 sylc ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) )
52 51 48 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ) ∧ ( ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) ∧ ( ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑄 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ∧ ( 𝑅 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) )