Metamath Proof Explorer

Theorem lshpkrcl

Description: The set G defined by hyperplane U is a linear functional. (Contributed by NM, 17-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 lshpkr.v 
 |-  V = ( Base ` W )
2 lshpkr.a 
 |-  .+ = ( +g ` W )
3 lshpkr.n 
 |-  N = ( LSpan ` W )
4 lshpkr.p 
 |-  .(+) = ( LSSum ` W )
5 lshpkr.h 
 |-  H = ( LSHyp ` W )
6 lshpkr.w 
 |-  ( ph -> W e. LVec )
7 lshpkr.u 
 |-  ( ph -> U e. H )
8 lshpkr.z 
 |-  ( ph -> Z e. V )
9 lshpkr.e 
 |-  ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
10 lshpkr.d 
 |-  D = ( Scalar ` W )
11 lshpkr.k 
 |-  K = ( Base ` D )
12 lshpkr.t 
 |-  .x. = ( .s ` W )
13 lshpkr.g 
 |-  G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
14 lshpkr.f 
 |-  F = ( LFnl ` W )
15 6 adantr 
 |-  ( ( ph /\ a e. V ) -> W e. LVec )
16 7 adantr 
 |-  ( ( ph /\ a e. V ) -> U e. H )
17 8 adantr 
 |-  ( ( ph /\ a e. V ) -> Z e. V )
18 simpr 
 |-  ( ( ph /\ a e. V ) -> a e. V )
19 9 adantr 
 |-  ( ( ph /\ a e. V ) -> ( U .(+) ( N ` { Z } ) ) = V )
20 1 2 3 4 5 15 16 17 18 19 10 11 12 lshpsmreu 
 |-  ( ( ph /\ a e. V ) -> E! k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) )
21 riotacl 
 |-  ( E! k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) -> ( iota_ k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) ) e. K )
22 20 21 syl 
 |-  ( ( ph /\ a e. V ) -> ( iota_ k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) ) e. K )
23 eqeq1 
 |-  ( x = a -> ( x = ( y .+ ( k .x. Z ) ) <-> a = ( y .+ ( k .x. Z ) ) ) )
24 23 rexbidv 
 |-  ( x = a -> ( E. y e. U x = ( y .+ ( k .x. Z ) ) <-> E. y e. U a = ( y .+ ( k .x. Z ) ) ) )
25 24 riotabidv 
 |-  ( x = a -> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) = ( iota_ k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) ) )
26 25 cbvmptv 
 |-  ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) ) = ( a e. V |-> ( iota_ k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) ) )
27 13 26 eqtri 
 |-  G = ( a e. V |-> ( iota_ k e. K E. y e. U a = ( y .+ ( k .x. Z ) ) ) )
28 22 27 fmptd 
 |-  ( ph -> G : V --> K )
29 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
30 1 2 3 4 5 6 7 8 8 9 10 11 12 29 13 lshpkrlem6 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )
31 30 ralrimivvva 
 |-  ( ph -> A. l e. K A. u e. V A. v e. V ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )
32 eqid 
 |-  ( +g ` D ) = ( +g ` D )
33 eqid 
 |-  ( .r ` D ) = ( .r ` D )
34 1 2 10 12 11 32 33 14 islfl 
 |-  ( W e. LVec -> ( G e. F <-> ( G : V --> K /\ A. l e. K A. u e. V A. v e. V ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) ) ) )
35 6 34 syl 
 |-  ( ph -> ( G e. F <-> ( G : V --> K /\ A. l e. K A. u e. V A. v e. V ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) ) ) )
36 28 31 35 mpbir2and 
 |-  ( ph -> G e. F )