Theorem lsatcmp2

Description: If an atom is included in at-most an atom, they are equal. More general version of lsatcmp . TODO: can lspsncmp shorten this? (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lsatcmp2.o	|- .0. = ( 0g ` W )
	lsatcmp2.a	|- A = ( LSAtoms ` W )
	lsatcmp2.w	|- ( ph -> W e. LVec )
	lsatcmp2.t	|- ( ph -> T e. A )
	lsatcmp2.u	|- ( ph -> ( U e. A \/ U = { .0. } ) )
Assertion	lsatcmp2	|- ( ph -> ( T C_ U <-> T = U ) )

Proof

Step	Hyp	Ref	Expression
1		lsatcmp2.o	|- .0. = ( 0g ` W )
2		lsatcmp2.a	|- A = ( LSAtoms ` W )
3		lsatcmp2.w	|- ( ph -> W e. LVec )
4		lsatcmp2.t	|- ( ph -> T e. A )
5		lsatcmp2.u	|- ( ph -> ( U e. A \/ U = { .0. } ) )
6		simpr	|- ( ( ph /\ T C_ U ) -> T C_ U )
7	3	adantr	|- ( ( ph /\ T C_ U ) -> W e. LVec )
8	4	adantr	|- ( ( ph /\ T C_ U ) -> T e. A )
9		lveclmod	|- ( W e. LVec -> W e. LMod )
10	3 9	syl	|- ( ph -> W e. LMod )
11	10	adantr	|- ( ( ph /\ T C_ U ) -> W e. LMod )
12	1 2 11 8 6	lsatssn0	|- ( ( ph /\ T C_ U ) -> U =/= { .0. } )
13	5	ord	|- ( ph -> ( -. U e. A -> U = { .0. } ) )
14	13	necon1ad	|- ( ph -> ( U =/= { .0. } -> U e. A ) )
15	14	adantr	|- ( ( ph /\ T C_ U ) -> ( U =/= { .0. } -> U e. A ) )
16	12 15	mpd	|- ( ( ph /\ T C_ U ) -> U e. A )
17	2 7 8 16	lsatcmp	|- ( ( ph /\ T C_ U ) -> ( T C_ U <-> T = U ) )
18	6 17	mpbid	|- ( ( ph /\ T C_ U ) -> T = U )
19	18	ex	|- ( ph -> ( T C_ U -> T = U ) )
20		eqimss	|- ( T = U -> T C_ U )
21	19 20	impbid1	|- ( ph -> ( T C_ U <-> T = U ) )