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 𝐵 = ( Base ‘ 𝐾 )
atcvreq0.l = ( le ‘ 𝐾 )
atcvreq0.z 0 = ( 0. ‘ 𝐾 )
atcvreq0.c 𝐶 = ( ⋖ ‘ 𝐾 )
atcvreq0.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atcvreq0 ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → ( 𝑋 𝐶 𝑃𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 atcvreq0.b 𝐵 = ( Base ‘ 𝐾 )
2 atcvreq0.l = ( le ‘ 𝐾 )
3 atcvreq0.z 0 = ( 0. ‘ 𝐾 )
4 atcvreq0.c 𝐶 = ( ⋖ ‘ 𝐾 )
5 atcvreq0.a 𝐴 = ( Atoms ‘ 𝐾 )
6 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 1 6 3 atl0le ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵 ) → 0 ( le ‘ 𝐾 ) 𝑋 )
8 7 3adant3 ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → 0 ( le ‘ 𝐾 ) 𝑋 )
9 8 adantr ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 0 ( le ‘ 𝐾 ) 𝑋 )
10 1 5 atbase ( 𝑃𝐴𝑃𝐵 )
11 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
12 1 11 4 cvrlt ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐵 ) ∧ 𝑋 𝐶 𝑃 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑃 )
13 10 12 syl3anl3 ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑃 )
14 atlpos ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
15 14 3ad2ant1 ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → 𝐾 ∈ Poset )
16 15 adantr ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 𝐾 ∈ Poset )
17 1 3 atl0cl ( 𝐾 ∈ AtLat → 0𝐵 )
18 17 3ad2ant1 ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → 0𝐵 )
19 18 adantr ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 0𝐵 )
20 10 3ad2ant3 ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → 𝑃𝐵 )
21 20 adantr ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 𝑃𝐵 )
22 simpl2 ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 𝑋𝐵 )
23 3 4 5 atcvr0 ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴 ) → 0 𝐶 𝑃 )
24 23 3adant2 ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → 0 𝐶 𝑃 )
25 24 adantr ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 0 𝐶 𝑃 )
26 1 6 11 4 cvrnbtwn3 ( ( 𝐾 ∈ Poset ∧ ( 0𝐵𝑃𝐵𝑋𝐵 ) ∧ 0 𝐶 𝑃 ) → ( ( 0 ( le ‘ 𝐾 ) 𝑋𝑋 ( lt ‘ 𝐾 ) 𝑃 ) ↔ 0 = 𝑋 ) )
27 16 19 21 22 25 26 syl131anc ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → ( ( 0 ( le ‘ 𝐾 ) 𝑋𝑋 ( lt ‘ 𝐾 ) 𝑃 ) ↔ 0 = 𝑋 ) )
28 9 13 27 mpbi2and ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 0 = 𝑋 )
29 28 eqcomd ( ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) ∧ 𝑋 𝐶 𝑃 ) → 𝑋 = 0 )
30 29 ex ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → ( 𝑋 𝐶 𝑃𝑋 = 0 ) )
31 breq1 ( 𝑋 = 0 → ( 𝑋 𝐶 𝑃0 𝐶 𝑃 ) )
32 24 31 syl5ibrcom ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → ( 𝑋 = 0𝑋 𝐶 𝑃 ) )
33 30 32 impbid ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑃𝐴 ) → ( 𝑋 𝐶 𝑃𝑋 = 0 ) )