Metamath Proof Explorer


Theorem cdleme0cp

Description: Part of proof of Lemma E in Crawley p. 113. TODO: Reformat as in cdlemg3a - swap consequent equality; make antecedent use df-3an . (Contributed by NM, 13-Jun-2012)

Ref Expression
Hypotheses cdleme0.l = ( le ‘ 𝐾 )
cdleme0.j = ( join ‘ 𝐾 )
cdleme0.m = ( meet ‘ 𝐾 )
cdleme0.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme0.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
Assertion cdleme0cp ( ( ( 𝐾 ∈ 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 simprll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝑃𝐴 )
10 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
11 10 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝐾 ∈ Lat )
12 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
14 9 13 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
15 simprr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝑄𝐴 )
16 12 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
17 15 16 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
18 12 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
19 11 14 17 18 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
20 12 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
21 20 ad2antlr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 1 2 4 hlatlej1 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → 𝑃 ( 𝑃 𝑄 ) )
23 8 9 15 22 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝑃 ( 𝑃 𝑄 ) )
24 12 1 2 3 4 atmod3i1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴 ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ( 𝑃 𝑄 ) ) → ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( ( 𝑃 𝑄 ) ( 𝑃 𝑊 ) ) )
25 8 9 19 21 23 24 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( ( 𝑃 𝑄 ) ( 𝑃 𝑊 ) ) )
26 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
27 1 2 26 4 5 lhpjat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 𝑊 ) = ( 1. ‘ 𝐾 ) )
28 27 adantrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( 𝑃 𝑊 ) = ( 1. ‘ 𝐾 ) )
29 28 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑃 𝑊 ) ) = ( ( 𝑃 𝑄 ) ( 1. ‘ 𝐾 ) ) )
30 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
31 30 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → 𝐾 ∈ OL )
32 12 3 26 olm11 ( ( 𝐾 ∈ OL ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 𝑄 ) )
33 31 19 32 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 𝑄 ) )
34 25 29 33 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( 𝑃 𝑄 ) )
35 7 34 syl5eq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( 𝑃 𝑈 ) = ( 𝑃 𝑄 ) )