Metamath Proof Explorer


Theorem lhpexle2lem

Description: Lemma for lhpexle2 . (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses lhpex1.l = ( le ‘ 𝐾 )
lhpex1.a 𝐴 = ( Atoms ‘ 𝐾 )
lhpex1.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle2lem ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l = ( le ‘ 𝐾 )
2 lhpex1.a 𝐴 = ( Atoms ‘ 𝐾 )
3 lhpex1.h 𝐻 = ( LHyp ‘ 𝐾 )
4 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
5 1 2 3 lhpexle1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋 ) )
6 4 5 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋 ) )
7 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 𝑊𝑝𝑋 ) ) → 𝑝 𝑊 )
8 simp3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 𝑊𝑝𝑋 ) ) → 𝑝𝑋 )
9 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 𝑊𝑝𝑋 ) ) → 𝑋 = 𝑌 )
10 8 9 neeqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 𝑊𝑝𝑋 ) ) → 𝑝𝑌 )
11 7 8 10 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ∧ ( 𝑝 𝑊𝑝𝑋 ) ) → ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )
12 11 3expia ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( ( 𝑝 𝑊𝑝𝑋 ) → ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ) )
13 12 reximdv ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ( ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ) )
14 6 13 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )
15 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → 𝐾 ∈ HL )
16 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → 𝑋𝐴 )
17 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → 𝑌𝐴 )
18 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → 𝑋𝑌 )
19 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
20 1 19 2 hlsupr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴 ) ∧ 𝑋𝑌 ) → ∃ 𝑝𝐴 ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
21 15 16 17 18 20 syl31anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → ∃ 𝑝𝐴 ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
22 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
23 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝐾 ∈ HL )
24 23 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝐾 ∈ Lat )
25 simprlr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝𝐴 )
26 22 2 atbase ( 𝑝𝐴𝑝 ∈ ( Base ‘ 𝐾 ) )
27 25 26 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
28 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋𝐴 )
29 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌𝐴 )
30 22 19 2 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴 ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
31 23 28 29 30 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
32 simpl1r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑊𝐻 )
33 22 3 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
34 32 33 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
35 simprr3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
36 simpl2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 𝑊 )
37 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 𝑊 )
38 22 2 atbase ( 𝑋𝐴𝑋 ∈ ( Base ‘ 𝐾 ) )
39 28 38 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
40 22 2 atbase ( 𝑌𝐴𝑌 ∈ ( Base ‘ 𝐾 ) )
41 29 40 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
42 22 1 19 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑋 𝑊𝑌 𝑊 ) ↔ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) 𝑊 ) )
43 24 39 41 34 42 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( ( 𝑋 𝑊𝑌 𝑊 ) ↔ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) 𝑊 ) )
44 36 37 43 mpbi2and ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) 𝑊 )
45 22 1 24 27 31 34 35 44 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝 𝑊 )
46 simprr1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝𝑋 )
47 simprr2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → 𝑝𝑌 )
48 45 46 47 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( ( 𝑋𝑌𝑝𝐴 ) ∧ ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) ) ) → ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )
49 48 exp44 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ( 𝑋𝑌 → ( 𝑝𝐴 → ( ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ) ) ) )
50 49 imp31 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) ∧ 𝑝𝐴 ) → ( ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ) )
51 50 reximdva ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → ( ∃ 𝑝𝐴 ( 𝑝𝑋𝑝𝑌𝑝 ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ) )
52 21 51 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ 𝑋𝑌 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )
53 14 52 pm2.61dane ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )