Metamath Proof Explorer


Theorem lhpelim

Description: Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 lhpelim.b 𝐵 = ( Base ‘ 𝐾 )
2 lhpelim.l = ( le ‘ 𝐾 )
3 lhpelim.j = ( join ‘ 𝐾 )
4 lhpelim.m = ( meet ‘ 𝐾 )
5 lhpelim.a 𝐴 = ( Atoms ‘ 𝐾 )
6 lhpelim.h 𝐻 = ( LHyp ‘ 𝐾 )
7 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
8 2 4 7 5 6 lhpmat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 𝑊 ) = ( 0. ‘ 𝐾 ) )
9 8 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( 𝑃 𝑊 ) = ( 0. ‘ 𝐾 ) )
10 9 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( ( 𝑃 𝑊 ) ( 𝑋 𝑊 ) ) = ( ( 0. ‘ 𝐾 ) ( 𝑋 𝑊 ) ) )
11 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝐾 ∈ HL )
12 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝑃𝐴 )
13 11 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝐾 ∈ Lat )
14 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝑋𝐵 )
15 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝑊𝐻 )
16 1 6 lhpbase ( 𝑊𝐻𝑊𝐵 )
17 15 16 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝑊𝐵 )
18 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵 ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
19 13 14 17 18 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
20 1 2 4 latmle2 ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵 ) → ( 𝑋 𝑊 ) 𝑊 )
21 13 14 17 20 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( 𝑋 𝑊 ) 𝑊 )
22 1 2 3 4 5 atmod4i2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴 ∧ ( 𝑋 𝑊 ) ∈ 𝐵𝑊𝐵 ) ∧ ( 𝑋 𝑊 ) 𝑊 ) → ( ( 𝑃 𝑊 ) ( 𝑋 𝑊 ) ) = ( ( 𝑃 ( 𝑋 𝑊 ) ) 𝑊 ) )
23 11 12 19 17 21 22 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( ( 𝑃 𝑊 ) ( 𝑋 𝑊 ) ) = ( ( 𝑃 ( 𝑋 𝑊 ) ) 𝑊 ) )
24 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
25 11 24 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → 𝐾 ∈ OL )
26 1 3 7 olj02 ( ( 𝐾 ∈ OL ∧ ( 𝑋 𝑊 ) ∈ 𝐵 ) → ( ( 0. ‘ 𝐾 ) ( 𝑋 𝑊 ) ) = ( 𝑋 𝑊 ) )
27 25 19 26 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( ( 0. ‘ 𝐾 ) ( 𝑋 𝑊 ) ) = ( 𝑋 𝑊 ) )
28 10 23 27 3eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑋𝐵 ) → ( ( 𝑃 ( 𝑋 𝑊 ) ) 𝑊 ) = ( 𝑋 𝑊 ) )