Theorem atcvr0

Description: An atom covers zero. ( atcv0 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	atomcvr0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	atomcvr0.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	atomcvr0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atcvr0	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴 ) → 0 𝐶 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		atomcvr0.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		atomcvr0.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		atomcvr0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5	4 1 2 3	isat	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑃 ∈ 𝐴 ↔ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 0 𝐶 𝑃 ) ) )
6	5	simplbda	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴 ) → 0 𝐶 𝑃 )