Metamath Proof Explorer


Theorem cdleme0cq

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 25-Apr-2013)

Ref Expression
Hypotheses cdleme0.l = ( le ‘ 𝐾 )
cdleme0.j = ( join ‘ 𝐾 )
cdleme0.m = ( meet ‘ 𝐾 )
cdleme0.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme0.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
Assertion cdleme0cq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( 𝑄 𝑈 ) = ( 𝑃 𝑄 ) )

Proof

Step Hyp Ref Expression
1 cdleme0.l = ( le ‘ 𝐾 )
2 cdleme0.j = ( join ‘ 𝐾 )
3 cdleme0.m = ( meet ‘ 𝐾 )
4 cdleme0.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme0.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 6 oveq2i ( 𝑄 𝑈 ) = ( 𝑄 ( ( 𝑃 𝑄 ) 𝑊 ) )
8 simpll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝐾 ∈ HL )
9 simprrl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝑄𝐴 )
10 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
11 10 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝐾 ∈ Lat )
12 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
14 13 ad2antrl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
15 12 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
16 9 15 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
17 12 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
18 11 14 16 17 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
19 12 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
20 19 ad2antlr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 12 1 2 latlej2 ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → 𝑄 ( 𝑃 𝑄 ) )
22 11 14 16 21 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝑄 ( 𝑃 𝑄 ) )
23 12 1 2 3 4 atmod3i1 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴 ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑄 ( 𝑃 𝑄 ) ) → ( 𝑄 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( ( 𝑃 𝑄 ) ( 𝑄 𝑊 ) ) )
24 8 9 18 20 22 23 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( 𝑄 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( ( 𝑃 𝑄 ) ( 𝑄 𝑊 ) ) )
25 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
26 1 2 25 4 5 lhpjat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝑄 𝑊 ) = ( 1. ‘ 𝐾 ) )
27 26 adantrl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( 𝑄 𝑊 ) = ( 1. ‘ 𝐾 ) )
28 27 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑄 𝑊 ) ) = ( ( 𝑃 𝑄 ) ( 1. ‘ 𝐾 ) ) )
29 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
30 29 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → 𝐾 ∈ OL )
31 12 3 25 olm11 ( ( 𝐾 ∈ OL ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 𝑄 ) )
32 30 18 31 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝑃 𝑄 ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 𝑄 ) )
33 24 28 32 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( 𝑄 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( 𝑃 𝑄 ) )
34 7 33 eqtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( 𝑄 𝑈 ) = ( 𝑃 𝑄 ) )