Theorem lshpkrlem2

Description: Lemma for lshpkrex . The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014)

	Ref	Expression
Hypotheses	lshpkrlem.v	|- V = ( Base ` W )
	lshpkrlem.a	|- .+ = ( +g ` W )
	lshpkrlem.n	|- N = ( LSpan ` W )
	lshpkrlem.p	|- .(+) = ( LSSum ` W )
	lshpkrlem.h	|- H = ( LSHyp ` W )
	lshpkrlem.w	|- ( ph -> W e. LVec )
	lshpkrlem.u	|- ( ph -> U e. H )
	lshpkrlem.z	|- ( ph -> Z e. V )
	lshpkrlem.x	|- ( ph -> X e. V )
	lshpkrlem.e	|- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
	lshpkrlem.d	|- D = ( Scalar ` W )
	lshpkrlem.k	|- K = ( Base ` D )
	lshpkrlem.t	|- .x. = ( .s ` W )
	lshpkrlem.o	|- .0. = ( 0g ` D )
	lshpkrlem.g	|- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
Assertion	lshpkrlem2	|- ( ph -> ( G ` X ) e. K )

Proof

Step	Hyp	Ref	Expression
1		lshpkrlem.v	|- V = ( Base ` W )
2		lshpkrlem.a	|- .+ = ( +g ` W )
3		lshpkrlem.n	|- N = ( LSpan ` W )
4		lshpkrlem.p	|- .(+) = ( LSSum ` W )
5		lshpkrlem.h	|- H = ( LSHyp ` W )
6		lshpkrlem.w	|- ( ph -> W e. LVec )
7		lshpkrlem.u	|- ( ph -> U e. H )
8		lshpkrlem.z	|- ( ph -> Z e. V )
9		lshpkrlem.x	|- ( ph -> X e. V )
10		lshpkrlem.e	|- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
11		lshpkrlem.d	|- D = ( Scalar ` W )
12		lshpkrlem.k	|- K = ( Base ` D )
13		lshpkrlem.t	|- .x. = ( .s ` W )
14		lshpkrlem.o	|- .0. = ( 0g ` D )
15		lshpkrlem.g	|- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
16		eqeq1	|- ( x = X -> ( x = ( y .+ ( k .x. Z ) ) <-> X = ( y .+ ( k .x. Z ) ) ) )
17	16	rexbidv	|- ( x = X -> ( E. y e. U x = ( y .+ ( k .x. Z ) ) <-> E. y e. U X = ( y .+ ( k .x. Z ) ) ) )
18	17	riotabidv	|- ( x = X -> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) = ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) )
19		riotaex	|- ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) e. _V
20	18 15 19	fvmpt	|- ( X e. V -> ( G ` X ) = ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) )
21	9 20	syl	|- ( ph -> ( G ` X ) = ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) )
22	1 2 3 4 5 6 7 8 9 10 11 12 13	lshpsmreu	|- ( ph -> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )
23		riotacl	|- ( E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) -> ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) e. K )
24	22 23	syl	|- ( ph -> ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) e. K )
25	21 24	eqeltrd	|- ( ph -> ( G ` X ) e. K )