Metamath Proof Explorer


Theorem cdleme15b

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, showing, in their notation, (p \/ s_1) /\ (q \/ s_1)=s_1. We represent s_1 with C . (Contributed by NM, 10-Oct-2012)

Ref Expression
Hypotheses cdleme12.l = ( le ‘ 𝐾 )
cdleme12.j = ( join ‘ 𝐾 )
cdleme12.m = ( meet ‘ 𝐾 )
cdleme12.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme12.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme12.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme12.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
cdleme12.g 𝐺 = ( ( 𝑇 𝑈 ) ( 𝑄 ( ( 𝑃 𝑇 ) 𝑊 ) ) )
cdleme15.c 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
cdleme15.x 𝑋 = ( ( 𝑃 𝑇 ) 𝑊 )
Assertion cdleme15b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 𝑃 𝐶 ) ( 𝑄 𝐶 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme12.l = ( le ‘ 𝐾 )
2 cdleme12.j = ( join ‘ 𝐾 )
3 cdleme12.m = ( meet ‘ 𝐾 )
4 cdleme12.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme12.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme12.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme12.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
8 cdleme12.g 𝐺 = ( ( 𝑇 𝑈 ) ( 𝑄 ( ( 𝑃 𝑇 ) 𝑊 ) ) )
9 cdleme15.c 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
10 cdleme15.x 𝑋 = ( ( 𝑃 𝑇 ) 𝑊 )
11 9 oveq2i ( 𝑃 𝐶 ) = ( 𝑃 ( ( 𝑃 𝑆 ) 𝑊 ) )
12 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ HL )
13 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑃𝐴 )
14 simp21l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑆𝐴 )
15 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 15 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴 ) → ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17 12 13 14 16 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑊𝐻 )
19 15 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 1 2 4 hlatlej1 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴 ) → 𝑃 ( 𝑃 𝑆 ) )
22 12 13 14 21 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑃 ( 𝑃 𝑆 ) )
23 15 1 2 3 4 atmod3i1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴 ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ( 𝑃 𝑆 ) ) → ( 𝑃 ( ( 𝑃 𝑆 ) 𝑊 ) ) = ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) )
24 12 13 17 20 22 23 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑃 ( ( 𝑃 𝑆 ) 𝑊 ) ) = ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) )
25 11 24 syl5eq ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑃 𝐶 ) = ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) )
26 25 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 𝑃 𝐶 ) 𝑄 ) = ( ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) 𝑄 ) )
27 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
28 12 27 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ OL )
29 12 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ Lat )
30 15 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
31 13 30 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 15 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
33 29 31 20 32 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑃 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
34 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑄𝐴 )
35 15 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
36 34 35 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
37 15 3 latmrot ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) 𝑄 ) = ( ( 𝑄 ( 𝑃 𝑆 ) ) ( 𝑃 𝑊 ) ) )
38 28 17 33 36 37 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) 𝑄 ) = ( ( 𝑄 ( 𝑃 𝑆 ) ) ( 𝑃 𝑊 ) ) )
39 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
40 simp23l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑃𝑄 )
41 40 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝑄𝑃 )
42 1 2 4 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑆𝐴𝑃𝐴 ) ∧ 𝑄𝑃 ) → ( 𝑄 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝑄 ) ) )
43 12 34 14 13 41 42 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑄 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝑄 ) ) )
44 39 43 mtod ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ¬ 𝑄 ( 𝑃 𝑆 ) )
45 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
46 12 45 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝐾 ∈ AtLat )
47 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
48 15 1 3 47 4 atnle ( ( 𝐾 ∈ AtLat ∧ 𝑄𝐴 ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ¬ 𝑄 ( 𝑃 𝑆 ) ↔ ( 𝑄 ( 𝑃 𝑆 ) ) = ( 0. ‘ 𝐾 ) ) )
49 46 34 17 48 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ¬ 𝑄 ( 𝑃 𝑆 ) ↔ ( 𝑄 ( 𝑃 𝑆 ) ) = ( 0. ‘ 𝐾 ) ) )
50 44 49 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑄 ( 𝑃 𝑆 ) ) = ( 0. ‘ 𝐾 ) )
51 50 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 𝑄 ( 𝑃 𝑆 ) ) ( 𝑃 𝑊 ) ) = ( ( 0. ‘ 𝐾 ) ( 𝑃 𝑊 ) ) )
52 15 3 47 olm02 ( ( 𝐾 ∈ OL ∧ ( 𝑃 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ( 𝑃 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
53 28 33 52 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 0. ‘ 𝐾 ) ( 𝑃 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
54 38 51 53 3eqtrrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 0. ‘ 𝐾 ) = ( ( ( 𝑃 𝑆 ) ( 𝑃 𝑊 ) ) 𝑄 ) )
55 26 54 eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 𝑃 𝐶 ) 𝑄 ) = ( 0. ‘ 𝐾 ) )
56 55 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( ( 𝑃 𝐶 ) 𝑄 ) 𝐶 ) = ( ( 0. ‘ 𝐾 ) 𝐶 ) )
57 15 2 3 4 5 9 cdleme9b ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑆𝐴𝑊𝐻 ) ) → 𝐶 ∈ ( Base ‘ 𝐾 ) )
58 12 13 14 18 57 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝐶 ∈ ( Base ‘ 𝐾 ) )
59 15 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
60 29 31 58 59 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( 𝑃 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
61 15 1 2 latlej2 ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → 𝐶 ( 𝑃 𝐶 ) )
62 29 31 58 61 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → 𝐶 ( 𝑃 𝐶 ) )
63 15 1 2 3 4 atmod2i2 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴 ∧ ( 𝑃 𝐶 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝐶 ( 𝑃 𝐶 ) ) → ( ( ( 𝑃 𝐶 ) 𝑄 ) 𝐶 ) = ( ( 𝑃 𝐶 ) ( 𝑄 𝐶 ) ) )
64 12 34 60 58 62 63 syl131anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( ( 𝑃 𝐶 ) 𝑄 ) 𝐶 ) = ( ( 𝑃 𝐶 ) ( 𝑄 𝐶 ) ) )
65 15 2 47 olj02 ( ( 𝐾 ∈ OL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) 𝐶 ) = 𝐶 )
66 28 58 65 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 0. ‘ 𝐾 ) 𝐶 ) = 𝐶 )
67 56 64 66 3eqtr3d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑇 𝑊 ) ∧ ( 𝑃𝑄𝑆𝑇 ) ) ∧ ( ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ∧ ¬ 𝑈 ( 𝑆 𝑇 ) ) ) → ( ( 𝑃 𝐶 ) ( 𝑄 𝐶 ) ) = 𝐶 )