Metamath Proof Explorer

Theorem lhpj1

Description: The join of a co-atom (hyperplane) and an element not under it is the lattice unity. (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses lhpj1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpj1.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpj1.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpj1.u ⊢ 1 = ( 1. ‘ 𝐾 )
lhpj1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpj1 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑋 ) = 1 )

Proof

Step Hyp Ref Expression
1 lhpj1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhpj1.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lhpj1.j ⊢ ∨ = ( join ‘ 𝐾 )
4 lhpj1.u ⊢ 1 = ( 1. ‘ 𝐾 )
5 lhpj1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ HL )
7 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
9 8 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑊 ∈ 𝐵 )
10 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
11 1 2 10 hlrelat2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑊 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) )
12 6 7 9 11 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑊 ↔ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) )
13 simp1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
15 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ¬ 𝑝 ≤ 𝑊 )
16 2 3 4 10 5 lhpjat1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑝 ) = 1 )
17 13 14 15 16 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑝 ) = 1 )
18 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝑝 ≤ 𝑋 )
19 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
20 19 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
21 1 10 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
22 21 3ad2ant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝑝 ∈ 𝐵 )
23 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
24 9 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
25 1 2 3 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( 𝑝 ≤ 𝑋 → ( 𝑊 ∨ 𝑝 ) ≤ ( 𝑊 ∨ 𝑋 ) ) )
26 20 22 23 24 25 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑝 ≤ 𝑋 → ( 𝑊 ∨ 𝑝 ) ≤ ( 𝑊 ∨ 𝑋 ) ) )
27 18 26 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑝 ) ≤ ( 𝑊 ∨ 𝑋 ) )
28 17 27 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 1 ≤ ( 𝑊 ∨ 𝑋 ) )
29 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
30 19 29 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝐾 ∈ OP )
31 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑊 ∨ 𝑋 ) ∈ 𝐵 )
32 20 24 23 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑋 ) ∈ 𝐵 )
33 1 2 4 op1le ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑊 ∨ 𝑋 ) ∈ 𝐵 ) → ( 1 ≤ ( 𝑊 ∨ 𝑋 ) ↔ ( 𝑊 ∨ 𝑋 ) = 1 ) )
34 30 32 33 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 1 ≤ ( 𝑊 ∨ 𝑋 ) ↔ ( 𝑊 ∨ 𝑋 ) = 1 ) )
35 28 34 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑋 ) = 1 )
36 35 rexlimdv3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑊 ) → ( 𝑊 ∨ 𝑋 ) = 1 ) )
37 12 36 sylbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑊 → ( 𝑊 ∨ 𝑋 ) = 1 ) )
38 37 impr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑋 ) = 1 )