Theorem atcv0eq

Description: Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	atcv0eq	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( 0H A = B ) )

Proof

Step	Hyp	Ref	Expression
1		atnemeq0	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( A i^i B ) = 0H ) )
2		atelch	|- ( A e. HAtoms -> A e. CH )
3		cvp	|- ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A
4	2 3	sylan	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A
5		atcv0	|- ( A e. HAtoms -> 0H
6	5	adantr	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> 0H
7	6	biantrurd	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A ( 0H
8	1 4 7	3bitrd	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B <-> ( 0H
9		atelch	|- ( B e. HAtoms -> B e. CH )
10		chjcl	|- ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )
11		h0elch	|- 0H e. CH
12		cvntr	|- ( ( 0H e. CH /\ A e. CH /\ ( A vH B ) e. CH ) -> ( ( 0H -. 0H
13	11 12	mp3an1	|- ( ( A e. CH /\ ( A vH B ) e. CH ) -> ( ( 0H -. 0H
14	10 13	syldan	|- ( ( A e. CH /\ B e. CH ) -> ( ( 0H -. 0H
15	2 9 14	syl2an	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( ( 0H -. 0H
16	8 15	sylbid	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B -> -. 0H
17	16	necon4ad	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( 0H A = B ) )
18		oveq1	|- ( A = B -> ( A vH B ) = ( B vH B ) )
19		chjidm	|- ( B e. CH -> ( B vH B ) = B )
20	9 19	syl	|- ( B e. HAtoms -> ( B vH B ) = B )
21	18 20	sylan9eq	|- ( ( A = B /\ B e. HAtoms ) -> ( A vH B ) = B )
22	21	eqcomd	|- ( ( A = B /\ B e. HAtoms ) -> B = ( A vH B ) )
23	22	eleq1d	|- ( ( A = B /\ B e. HAtoms ) -> ( B e. HAtoms <-> ( A vH B ) e. HAtoms ) )
24	23	ex	|- ( A = B -> ( B e. HAtoms -> ( B e. HAtoms <-> ( A vH B ) e. HAtoms ) ) )
25	24	ibd	|- ( A = B -> ( B e. HAtoms -> ( A vH B ) e. HAtoms ) )
26		atcv0	|- ( ( A vH B ) e. HAtoms -> 0H
27	25 26	syl6com	|- ( B e. HAtoms -> ( A = B -> 0H
28	27	adantl	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A = B -> 0H
29	17 28	impbid	|- ( ( A e. HAtoms /\ B e. HAtoms ) -> ( 0H A = B ) )