Theorem lcoval

Description: The value of a linear combination. (Contributed by AV, 5-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lcoop.b	|- B = ( Base ` M )
	lcoop.s	|- S = ( Scalar ` M )
	lcoop.r	|- R = ( Base ` S )
Assertion	lcoval	|- ( ( M e. X /\ V e. ~P B ) -> ( C e. ( M LinCo V ) <-> ( C e. B /\ E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ C = ( s ( linC ` M ) V ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcoop.b	|- B = ( Base ` M )
2		lcoop.s	|- S = ( Scalar ` M )
3		lcoop.r	|- R = ( Base ` S )
4	1 2 3	lcoop	|- ( ( M e. X /\ V e. ~P B ) -> ( M LinCo V ) = { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } )
5	4	eleq2d	|- ( ( M e. X /\ V e. ~P B ) -> ( C e. ( M LinCo V ) <-> C e. { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } ) )
6		eqeq1	|- ( c = C -> ( c = ( s ( linC ` M ) V ) <-> C = ( s ( linC ` M ) V ) ) )
7	6	anbi2d	|- ( c = C -> ( ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) <-> ( s finSupp ( 0g ` S ) /\ C = ( s ( linC ` M ) V ) ) ) )
8	7	rexbidv	|- ( c = C -> ( E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) <-> E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ C = ( s ( linC ` M ) V ) ) ) )
9	8	elrab	|- ( C e. { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } <-> ( C e. B /\ E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ C = ( s ( linC ` M ) V ) ) ) )
10	5 9	bitrdi	|- ( ( M e. X /\ V e. ~P B ) -> ( C e. ( M LinCo V ) <-> ( C e. B /\ E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ C = ( s ( linC ` M ) V ) ) ) ) )