Theorem lcvbr2

Description: The covers relation for a left vector space (or a left module). ( cvbr2 analog.) (Contributed by NM, 9-Jan-2015)

	Ref	Expression
Hypotheses	lcvfbr.s	|- S = ( LSubSp ` W )
	lcvfbr.c	|- C = (
	lcvfbr.w	|- ( ph -> W e. X )
	lcvfbr.t	|- ( ph -> T e. S )
	lcvfbr.u	|- ( ph -> U e. S )
Assertion	lcvbr2	|- ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcvfbr.s	|- S = ( LSubSp ` W )
2		lcvfbr.c	|- C = (
3		lcvfbr.w	|- ( ph -> W e. X )
4		lcvfbr.t	|- ( ph -> T e. S )
5		lcvfbr.u	|- ( ph -> U e. S )
6	1 2 3 4 5	lcvbr	|- ( ph -> ( T C U <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) ) )
7		iman	|- ( ( ( T C. s /\ s C_ U ) -> s = U ) <-> -. ( ( T C. s /\ s C_ U ) /\ -. s = U ) )
8		anass	|- ( ( ( T C. s /\ s C_ U ) /\ -. s = U ) <-> ( T C. s /\ ( s C_ U /\ -. s = U ) ) )
9		dfpss2	|- ( s C. U <-> ( s C_ U /\ -. s = U ) )
10	9	anbi2i	|- ( ( T C. s /\ s C. U ) <-> ( T C. s /\ ( s C_ U /\ -. s = U ) ) )
11	8 10	bitr4i	|- ( ( ( T C. s /\ s C_ U ) /\ -. s = U ) <-> ( T C. s /\ s C. U ) )
12	7 11	xchbinx	|- ( ( ( T C. s /\ s C_ U ) -> s = U ) <-> -. ( T C. s /\ s C. U ) )
13	12	ralbii	|- ( A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) <-> A. s e. S -. ( T C. s /\ s C. U ) )
14		ralnex	|- ( A. s e. S -. ( T C. s /\ s C. U ) <-> -. E. s e. S ( T C. s /\ s C. U ) )
15	13 14	bitri	|- ( A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) <-> -. E. s e. S ( T C. s /\ s C. U ) )
16	15	anbi2i	|- ( ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) ) <-> ( T C. U /\ -. E. s e. S ( T C. s /\ s C. U ) ) )
17	6 16	bitr4di	|- ( ph -> ( T C U <-> ( T C. U /\ A. s e. S ( ( T C. s /\ s C_ U ) -> s = U ) ) ) )