Metamath Proof Explorer

Theorem lhpmcvr

Description: The meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses lhpmcvr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpmcvr.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmcvr.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmcvr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
lhpmcvr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmcvr ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) 𝐶 𝑋 )

Proof

Step Hyp Ref Expression
1 lhpmcvr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhpmcvr.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lhpmcvr.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 lhpmcvr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 lhpmcvr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 6 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
8 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
9 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
10 9 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
11 1 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) = ( 𝑊 ∧ 𝑋 ) )
12 7 8 10 11 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) = ( 𝑊 ∧ 𝑋 ) )
13 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
14 13 4 5 lhp1cvr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 𝐶 ( 1. ‘ 𝐾 ) )
15 14 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝑊 𝐶 ( 1. ‘ 𝐾 ) )
16 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
17 1 2 16 13 5 lhpj1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑊 ( join ‘ 𝐾 ) 𝑋 ) = ( 1. ‘ 𝐾 ) )
18 15 17 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝑊 𝐶 ( 𝑊 ( join ‘ 𝐾 ) 𝑋 ) )
19 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
20 1 16 3 4 cvrexch ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑊 ∧ 𝑋 ) 𝐶 𝑋 ↔ 𝑊 𝐶 ( 𝑊 ( join ‘ 𝐾 ) 𝑋 ) ) )
21 19 10 8 20 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( ( 𝑊 ∧ 𝑋 ) 𝐶 𝑋 ↔ 𝑊 𝐶 ( 𝑊 ( join ‘ 𝐾 ) 𝑋 ) ) )
22 18 21 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑊 ∧ 𝑋 ) 𝐶 𝑋 )
23 12 22 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) 𝐶 𝑋 )