Theorem isssp

Description: The predicate "is a subspace." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isssp.g	|- G = ( +v ` U )
	isssp.f	|- F = ( +v ` W )
	isssp.s	|- S = ( .sOLD ` U )
	isssp.r	|- R = ( .sOLD ` W )
	isssp.n	|- N = ( normCV ` U )
	isssp.m	|- M = ( normCV ` W )
	isssp.h	|- H = ( SubSp ` U )
Assertion	isssp	|- ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isssp.g	|- G = ( +v ` U )
2		isssp.f	|- F = ( +v ` W )
3		isssp.s	|- S = ( .sOLD ` U )
4		isssp.r	|- R = ( .sOLD ` W )
5		isssp.n	|- N = ( normCV ` U )
6		isssp.m	|- M = ( normCV ` W )
7		isssp.h	|- H = ( SubSp ` U )
8	1 3 5 7	sspval	|- ( U e. NrmCVec -> H = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )
9	8	eleq2d	|- ( U e. NrmCVec -> ( W e. H <-> W e. { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } ) )
10		fveq2	|- ( w = W -> ( +v ` w ) = ( +v ` W ) )
11	10 2	eqtr4di	|- ( w = W -> ( +v ` w ) = F )
12	11	sseq1d	|- ( w = W -> ( ( +v ` w ) C_ G <-> F C_ G ) )
13		fveq2	|- ( w = W -> ( .sOLD ` w ) = ( .sOLD ` W ) )
14	13 4	eqtr4di	|- ( w = W -> ( .sOLD ` w ) = R )
15	14	sseq1d	|- ( w = W -> ( ( .sOLD ` w ) C_ S <-> R C_ S ) )
16		fveq2	|- ( w = W -> ( normCV ` w ) = ( normCV ` W ) )
17	16 6	eqtr4di	|- ( w = W -> ( normCV ` w ) = M )
18	17	sseq1d	|- ( w = W -> ( ( normCV ` w ) C_ N <-> M C_ N ) )
19	12 15 18	3anbi123d	|- ( w = W -> ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) <-> ( F C_ G /\ R C_ S /\ M C_ N ) ) )
20	19	elrab	|- ( W e. { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) )
21	9 20	bitrdi	|- ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) ) )