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

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 ) )