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

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