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
|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( A i^i B ) = 0H ) )

Proof

Step Hyp Ref Expression
1 atsseq
 |-  ( ( B e. HAtoms /\ A e. HAtoms ) -> ( B C_ A <-> B = A ) )
2 eqcom
 |-  ( B = A <-> A = B )
3 1 2 bitrdi
 |-  ( ( B e. HAtoms /\ A e. HAtoms ) -> ( B C_ A <-> A = B ) )
4 3 ancoms
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( B C_ A <-> A = B ) )
5 4 necon3bbid
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( -. B C_ A <-> A =/= B ) )
6 atelch
 |-  ( A e. HAtoms -> A e. CH )
7 atnssm0
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> ( A i^i B ) = 0H ) )
8 6 7 sylan
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( -. B C_ A <-> ( A i^i B ) = 0H ) )
9 5 8 bitr3d
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( A i^i B ) = 0H ) )