Metamath Proof Explorer


Theorem cdleme30a

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

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

Proof

Step Hyp Ref Expression
1 cdleme30.b 𝐵 = ( Base ‘ 𝐾 )
2 cdleme30.l = ( le ‘ 𝐾 )
3 cdleme30.j = ( join ‘ 𝐾 )
4 cdleme30.m = ( meet ‘ 𝐾 )
5 cdleme30.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme30.h 𝐻 = ( LHyp ‘ 𝐾 )
7 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝐾 ∈ HL )
8 7 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝐾 ∈ Lat )
9 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑠𝐴 )
10 1 5 atbase ( 𝑠𝐴𝑠𝐵 )
11 9 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑠𝐵 )
12 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑌𝐵 )
13 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑊𝐻 )
14 1 6 lhpbase ( 𝑊𝐻𝑊𝐵 )
15 13 14 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑊𝐵 )
16 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵 ) → ( 𝑌 𝑊 ) ∈ 𝐵 )
17 8 12 15 16 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑌 𝑊 ) ∈ 𝐵 )
18 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑋𝐵 )
19 1 3 latjass ( ( 𝐾 ∈ Lat ∧ ( 𝑠𝐵 ∧ ( 𝑌 𝑊 ) ∈ 𝐵𝑋𝐵 ) ) → ( ( 𝑠 ( 𝑌 𝑊 ) ) 𝑋 ) = ( 𝑠 ( ( 𝑌 𝑊 ) 𝑋 ) ) )
20 8 11 17 18 19 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( ( 𝑠 ( 𝑌 𝑊 ) ) 𝑋 ) = ( 𝑠 ( ( 𝑌 𝑊 ) 𝑋 ) ) )
21 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋 )
22 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑋 𝑌 )
23 1 2 4 latmlem1 ( ( 𝐾 ∈ Lat ∧ ( 𝑋𝐵𝑌𝐵𝑊𝐵 ) ) → ( 𝑋 𝑌 → ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) ) )
24 8 18 12 15 23 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑋 𝑌 → ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) ) )
25 22 24 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) )
26 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵 ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
27 8 18 15 26 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
28 1 2 3 latjlej2 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 𝑊 ) ∈ 𝐵𝑠𝐵 ) ) → ( ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) → ( 𝑠 ( 𝑋 𝑊 ) ) ( 𝑠 ( 𝑌 𝑊 ) ) ) )
29 8 27 17 11 28 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) → ( 𝑠 ( 𝑋 𝑊 ) ) ( 𝑠 ( 𝑌 𝑊 ) ) ) )
30 25 29 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( 𝑋 𝑊 ) ) ( 𝑠 ( 𝑌 𝑊 ) ) )
31 21 30 eqbrtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑋 ( 𝑠 ( 𝑌 𝑊 ) ) )
32 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑠𝐵 ∧ ( 𝑌 𝑊 ) ∈ 𝐵 ) → ( 𝑠 ( 𝑌 𝑊 ) ) ∈ 𝐵 )
33 8 11 17 32 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( 𝑌 𝑊 ) ) ∈ 𝐵 )
34 1 2 3 latleeqj2 ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ ( 𝑠 ( 𝑌 𝑊 ) ) ∈ 𝐵 ) → ( 𝑋 ( 𝑠 ( 𝑌 𝑊 ) ) ↔ ( ( 𝑠 ( 𝑌 𝑊 ) ) 𝑋 ) = ( 𝑠 ( 𝑌 𝑊 ) ) ) )
35 8 18 33 34 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑋 ( 𝑠 ( 𝑌 𝑊 ) ) ↔ ( ( 𝑠 ( 𝑌 𝑊 ) ) 𝑋 ) = ( 𝑠 ( 𝑌 𝑊 ) ) ) )
36 31 35 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( ( 𝑠 ( 𝑌 𝑊 ) ) 𝑋 ) = ( 𝑠 ( 𝑌 𝑊 ) ) )
37 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
38 1 2 3 4 6 lhpmod2i2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑌𝐵𝑋𝐵 ) ∧ 𝑋 𝑌 ) → ( ( 𝑌 𝑊 ) 𝑋 ) = ( 𝑌 ( 𝑊 𝑋 ) ) )
39 37 12 18 22 38 syl121anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( ( 𝑌 𝑊 ) 𝑋 ) = ( 𝑌 ( 𝑊 𝑋 ) ) )
40 39 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( ( 𝑌 𝑊 ) 𝑋 ) ) = ( 𝑠 ( 𝑌 ( 𝑊 𝑋 ) ) ) )
41 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) )
42 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
43 1 2 3 42 6 lhpj1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ) → ( 𝑊 𝑋 ) = ( 1. ‘ 𝐾 ) )
44 37 41 43 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑊 𝑋 ) = ( 1. ‘ 𝐾 ) )
45 44 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑌 ( 𝑊 𝑋 ) ) = ( 𝑌 ( 1. ‘ 𝐾 ) ) )
46 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
47 7 46 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝐾 ∈ OL )
48 1 4 42 olm11 ( ( 𝐾 ∈ OL ∧ 𝑌𝐵 ) → ( 𝑌 ( 1. ‘ 𝐾 ) ) = 𝑌 )
49 47 12 48 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑌 ( 1. ‘ 𝐾 ) ) = 𝑌 )
50 45 49 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑌 ( 𝑊 𝑋 ) ) = 𝑌 )
51 50 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( 𝑌 ( 𝑊 𝑋 ) ) ) = ( 𝑠 𝑌 ) )
52 1 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑠𝐵 ∧ ( 𝑋 𝑊 ) ∈ 𝐵 ) → 𝑠 ( 𝑠 ( 𝑋 𝑊 ) ) )
53 8 11 27 52 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑠 ( 𝑠 ( 𝑋 𝑊 ) ) )
54 53 21 breqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑠 𝑋 )
55 1 2 8 11 18 12 54 22 lattrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → 𝑠 𝑌 )
56 1 2 3 latleeqj1 ( ( 𝐾 ∈ Lat ∧ 𝑠𝐵𝑌𝐵 ) → ( 𝑠 𝑌 ↔ ( 𝑠 𝑌 ) = 𝑌 ) )
57 8 11 12 56 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 𝑌 ↔ ( 𝑠 𝑌 ) = 𝑌 ) )
58 55 57 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 𝑌 ) = 𝑌 )
59 40 51 58 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( ( 𝑌 𝑊 ) 𝑋 ) ) = 𝑌 )
60 20 36 59 3eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐴 ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ 𝑌𝐵 ) ∧ ( ( 𝑠 ( 𝑋 𝑊 ) ) = 𝑋𝑋 𝑌 ) ) → ( 𝑠 ( 𝑌 𝑊 ) ) = 𝑌 )