Metamath Proof Explorer

Theorem atcvreq0

Description: An element covered by an atom must be zero. ( atcveq0 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses atcvreq0.b ⊢ B = Base K
atcvreq0.l ⊢ ≤ ˙ = ≤ K
atcvreq0.z ⊢ 0 ˙ = 0. ⁡ K
atcvreq0.c ⊢ C = ⋖ K
atcvreq0.a ⊢ A = Atoms ⁡ K
Assertion atcvreq0 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → X C P ↔ X = 0 ˙

Proof

Step Hyp Ref Expression
1 atcvreq0.b ⊢ B = Base K
2 atcvreq0.l ⊢ ≤ ˙ = ≤ K
3 atcvreq0.z ⊢ 0 ˙ = 0. ⁡ K
4 atcvreq0.c ⊢ C = ⋖ K
5 atcvreq0.a ⊢ A = Atoms ⁡ K
6 eqid ⊢ ≤ K = ≤ K
7 1 6 3 atl0le ⊢ K ∈ AtLat ∧ X ∈ B → 0 ˙ ≤ K X
8 7 3adant3 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → 0 ˙ ≤ K X
9 8 adantr ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → 0 ˙ ≤ K X
10 1 5 atbase ⊢ P ∈ A → P ∈ B
11 eqid ⊢ < K = < K
12 1 11 4 cvrlt ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ B ∧ X C P → X < K P
13 10 12 syl3anl3 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → X < K P
14 atlpos ⊢ K ∈ AtLat → K ∈ Poset
15 14 3ad2ant1 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → K ∈ Poset
16 15 adantr ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → K ∈ Poset
17 1 3 atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ B
18 17 3ad2ant1 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → 0 ˙ ∈ B
19 18 adantr ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → 0 ˙ ∈ B
20 10 3ad2ant3 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → P ∈ B
21 20 adantr ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → P ∈ B
22 simpl2 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → X ∈ B
23 3 4 5 atcvr0 ⊢ K ∈ AtLat ∧ P ∈ A → 0 ˙ C P
24 23 3adant2 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → 0 ˙ C P
25 24 adantr ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → 0 ˙ C P
26 1 6 11 4 cvrnbtwn3 ⊢ K ∈ Poset ∧ 0 ˙ ∈ B ∧ P ∈ B ∧ X ∈ B ∧ 0 ˙ C P → 0 ˙ ≤ K X ∧ X < K P ↔ 0 ˙ = X
27 16 19 21 22 25 26 syl131anc ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → 0 ˙ ≤ K X ∧ X < K P ↔ 0 ˙ = X
28 9 13 27 mpbi2and ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → 0 ˙ = X
29 28 eqcomd ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ X C P → X = 0 ˙
30 29 ex ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → X C P → X = 0 ˙
31 breq1 ⊢ X = 0 ˙ → X C P ↔ 0 ˙ C P
32 24 31 syl5ibrcom ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → X = 0 ˙ → X C P
33 30 32 impbid ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A → X C P ↔ X = 0 ˙