Theorem isat2

Description: The predicate "is an atom". ( elatcv0 analog.) (Contributed by NM, 18-Jun-2012)

	Ref	Expression
Hypotheses	isatom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isatom.z	⊢ 0 = ( 0. ‘ 𝐾 )
	isatom.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	isatom.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	isat2	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑃 ∈ 𝐴 ↔ 0 𝐶 𝑃 ) )

Proof

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