Metamath Proof Explorer


Theorem cdlemc1

Description: Part of proof of Lemma C in Crawley p. 112. TODO: shorten with atmod3i1 ? (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemc1.b 𝐵 = ( Base ‘ 𝐾 )
cdlemc1.l = ( le ‘ 𝐾 )
cdlemc1.j = ( join ‘ 𝐾 )
cdlemc1.m = ( meet ‘ 𝐾 )
cdlemc1.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemc1.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemc1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( ( 𝑃 𝑋 ) 𝑊 ) ) = ( 𝑃 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cdlemc1.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemc1.l = ( le ‘ 𝐾 )
3 cdlemc1.j = ( join ‘ 𝐾 )
4 cdlemc1.m = ( meet ‘ 𝐾 )
5 cdlemc1.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemc1.h 𝐻 = ( LHyp ‘ 𝐾 )
7 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ HL )
8 7 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ Lat )
9 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃𝐴 )
10 1 5 atbase ( 𝑃𝐴𝑃𝐵 )
11 9 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃𝐵 )
12 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑋𝐵 )
13 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵 ) → ( 𝑃 𝑋 ) ∈ 𝐵 )
14 8 11 12 13 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 𝑋 ) ∈ 𝐵 )
15 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊𝐻 )
16 1 6 lhpbase ( 𝑊𝐻𝑊𝐵 )
17 15 16 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊𝐵 )
18 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑋 ) ∈ 𝐵𝑊𝐵 ) → ( ( 𝑃 𝑋 ) 𝑊 ) ∈ 𝐵 )
19 8 14 17 18 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 𝑋 ) 𝑊 ) ∈ 𝐵 )
20 1 3 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ( ( 𝑃 𝑋 ) 𝑊 ) ∈ 𝐵 ) → ( 𝑃 ( ( 𝑃 𝑋 ) 𝑊 ) ) = ( ( ( 𝑃 𝑋 ) 𝑊 ) 𝑃 ) )
21 8 11 19 20 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( ( 𝑃 𝑋 ) 𝑊 ) ) = ( ( ( 𝑃 𝑋 ) 𝑊 ) 𝑃 ) )
22 1 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵 ) → 𝑃 ( 𝑃 𝑋 ) )
23 8 11 12 22 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃 ( 𝑃 𝑋 ) )
24 1 2 3 4 5 atmod2i1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴 ∧ ( 𝑃 𝑋 ) ∈ 𝐵𝑊𝐵 ) ∧ 𝑃 ( 𝑃 𝑋 ) ) → ( ( ( 𝑃 𝑋 ) 𝑊 ) 𝑃 ) = ( ( 𝑃 𝑋 ) ( 𝑊 𝑃 ) ) )
25 7 9 14 17 23 24 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( ( 𝑃 𝑋 ) 𝑊 ) 𝑃 ) = ( ( 𝑃 𝑋 ) ( 𝑊 𝑃 ) ) )
26 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
27 2 3 26 5 6 lhpjat1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑊 𝑃 ) = ( 1. ‘ 𝐾 ) )
28 27 3adant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑊 𝑃 ) = ( 1. ‘ 𝐾 ) )
29 28 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 𝑋 ) ( 𝑊 𝑃 ) ) = ( ( 𝑃 𝑋 ) ( 1. ‘ 𝐾 ) ) )
30 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
31 7 30 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ OL )
32 1 4 26 olm11 ( ( 𝐾 ∈ OL ∧ ( 𝑃 𝑋 ) ∈ 𝐵 ) → ( ( 𝑃 𝑋 ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 𝑋 ) )
33 31 14 32 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 𝑋 ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 𝑋 ) )
34 29 33 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 𝑋 ) ( 𝑊 𝑃 ) ) = ( 𝑃 𝑋 ) )
35 21 25 34 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( ( 𝑃 𝑋 ) 𝑊 ) ) = ( 𝑃 𝑋 ) )