Metamath Proof Explorer


Theorem cdleme17c

Description: Part of proof of Lemma E in Crawley p. 114, first part of 4th paragraph. C represents s_1. We show, in their notation, (p \/ q) /\ (q \/ s_1)=q. (Contributed by NM, 11-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme17.l = ( le ‘ 𝐾 )
2 cdleme17.j = ( join ‘ 𝐾 )
3 cdleme17.m = ( meet ‘ 𝐾 )
4 cdleme17.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme17.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme17.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme17.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
8 cdleme17.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
9 cdleme17.c 𝐶 = ( ( 𝑃 𝑆 ) 𝑊 )
10 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
11 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
12 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
13 2 4 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) = ( 𝑄 𝑃 ) )
14 10 11 12 13 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑄 𝑃 ) )
15 14 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑄 𝐶 ) ) = ( ( 𝑄 𝑃 ) ( 𝑄 𝐶 ) ) )
16 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
17 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑃 𝑊 )
18 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
19 10 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
20 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21 20 4 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
22 18 21 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
23 20 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
24 11 23 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
25 20 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
26 12 25 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
27 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
28 20 1 2 latnlej1l ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑆𝑃 )
29 28 necomd ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑃𝑆 )
30 19 22 24 26 27 29 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝑆 )
31 1 2 3 4 5 9 cdleme9a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑆𝐴𝑃𝑆 ) ) → 𝐶𝐴 )
32 10 16 11 17 18 30 31 syl222anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐶𝐴 )
33 1 2 3 4 5 6 7 8 9 cdleme17b ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝐶 ( 𝑃 𝑄 ) )
34 1 2 3 4 2llnma1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝐶𝐴 ) ∧ ¬ 𝐶 ( 𝑃 𝑄 ) ) → ( ( 𝑄 𝑃 ) ( 𝑄 𝐶 ) ) = 𝑄 )
35 10 11 12 32 33 34 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑄 𝑃 ) ( 𝑄 𝐶 ) ) = 𝑄 )
36 15 35 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑄 𝐶 ) ) = 𝑄 )