Metamath Proof Explorer

Theorem cvlcvrp

Description: A Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlcvrp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvlcvrp.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlcvrp.m ⊢ ∧ = ( meet ‘ 𝐾 )
cvlcvrp.z ⊢ 0 = ( 0. ‘ 𝐾 )
cvlcvrp.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
cvlcvrp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlcvrp ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 0 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cvlcvrp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvlcvrp.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cvlcvrp.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cvlcvrp.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 cvlcvrp.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6 cvlcvrp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 simp13 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ CvLat )
8 cvllat ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ Lat )
9 7 8 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ Lat )
10 simp2 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
11 1 6 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
12 11 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
13 1 3 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑃 ) = ( 𝑃 ∧ 𝑋 ) )
14 9 10 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∧ 𝑃 ) = ( 𝑃 ∧ 𝑋 ) )
15 14 eqeq1d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 0 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
16 cvlatl ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )
17 7 16 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
18 simp3 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
19 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
20 1 19 3 4 6 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
21 17 18 10 20 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
22 1 19 2 5 6 cvlcvr1 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )
23 15 21 22 3bitr2d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑋 ∧ 𝑃 ) = 0 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )