This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscvlat2N

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses iscvlat2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
iscvlat2.l ⊢ ≤ = ( le ‘ 𝐾 )
iscvlat2.j ⊢ ∨ = ( join ‘ 𝐾 )
iscvlat2.m ⊢ ∧ = ( meet ‘ 𝐾 )
iscvlat2.z ⊢ 0 = ( 0. ‘ 𝐾 )
iscvlat2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion iscvlat2N ( 𝐾 ∈ CvLat ↔ ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscvlat2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 iscvlat2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 iscvlat2.j ⊢ ∨ = ( join ‘ 𝐾 )
4 iscvlat2.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 iscvlat2.z ⊢ 0 = ( 0. ‘ 𝐾 )
6 iscvlat2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 1 2 3 6 iscvlat ⊢ ( 𝐾 ∈ CvLat ↔ ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )
8 simpll ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
9 simplrl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑝 ∈ 𝐴 )
10 simpr ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
11 1 2 4 5 6 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑝 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑝 ≤ 𝑥 ↔ ( 𝑝 ∧ 𝑥 ) = 0 ) )
12 8 9 10 11 syl3anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑝 ≤ 𝑥 ↔ ( 𝑝 ∧ 𝑥 ) = 0 ) )
13 12 anbi1d ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) ↔ ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) ) )
14 13 imbi1d ⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ↔ ( ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )
15 14 ralbidva ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )
16 15 2ralbidva ⊢ ( 𝐾 ∈ AtLat → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )
17 16 pm5.32i ⊢ ( ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) ↔ ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )
18 7 17 bitri ⊢ ( 𝐾 ∈ CvLat ↔ ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑝 ∧ 𝑥 ) = 0 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )