Metamath Proof Explorer


Theorem atnemeq0

Description: The meet of distinct atoms is the zero subspace. (Contributed by NM, 25-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atnemeq0 ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 atsseq ( ( 𝐵 ∈ HAtoms ∧ 𝐴 ∈ HAtoms ) → ( 𝐵𝐴𝐵 = 𝐴 ) )
2 eqcom ( 𝐵 = 𝐴𝐴 = 𝐵 )
3 1 2 bitrdi ( ( 𝐵 ∈ HAtoms ∧ 𝐴 ∈ HAtoms ) → ( 𝐵𝐴𝐴 = 𝐵 ) )
4 3 ancoms ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐵𝐴𝐴 = 𝐵 ) )
5 4 necon3bbid ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵𝐴𝐴𝐵 ) )
6 atelch ( 𝐴 ∈ HAtoms → 𝐴C )
7 atnssm0 ( ( 𝐴C𝐵 ∈ HAtoms ) → ( ¬ 𝐵𝐴 ↔ ( 𝐴𝐵 ) = 0 ) )
8 6 7 sylan ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵𝐴 ↔ ( 𝐴𝐵 ) = 0 ) )
9 5 8 bitr3d ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 0 ) )