Metamath Proof Explorer

Theorem lshpkrlem3

Description: Lemma for lshpkrex . Defining property of GX . (Contributed by NM, 15-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 lshpkrlem3 
|- ( ph -> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) )

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 1 2 3 4 5 6 7 8 9 10 11 12 13 lshpsmreu 
 |-  ( ph -> E! l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) )
17 riotasbc 
 |-  ( E! l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) -> [. ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) )
18 16 17 syl 
 |-  ( ph -> [. ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) )
19 eqeq1 
 |-  ( x = X -> ( x = ( z .+ ( l .x. Z ) ) <-> X = ( z .+ ( l .x. Z ) ) ) )
20 19 rexbidv 
 |-  ( x = X -> ( E. z e. U x = ( z .+ ( l .x. Z ) ) <-> E. z e. U X = ( z .+ ( l .x. Z ) ) ) )
21 20 riotabidv 
 |-  ( x = X -> ( iota_ l e. K E. z e. U x = ( z .+ ( l .x. Z ) ) ) = ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) )
22 oveq1 
 |-  ( k = l -> ( k .x. Z ) = ( l .x. Z ) )
23 22 oveq2d 
 |-  ( k = l -> ( y .+ ( k .x. Z ) ) = ( y .+ ( l .x. Z ) ) )
24 23 eqeq2d 
 |-  ( k = l -> ( x = ( y .+ ( k .x. Z ) ) <-> x = ( y .+ ( l .x. Z ) ) ) )
25 24 rexbidv 
 |-  ( k = l -> ( E. y e. U x = ( y .+ ( k .x. Z ) ) <-> E. y e. U x = ( y .+ ( l .x. Z ) ) ) )
26 oveq1 
 |-  ( y = z -> ( y .+ ( l .x. Z ) ) = ( z .+ ( l .x. Z ) ) )
27 26 eqeq2d 
 |-  ( y = z -> ( x = ( y .+ ( l .x. Z ) ) <-> x = ( z .+ ( l .x. Z ) ) ) )
28 27 cbvrexvw 
 |-  ( E. y e. U x = ( y .+ ( l .x. Z ) ) <-> E. z e. U x = ( z .+ ( l .x. Z ) ) )
29 25 28 bitrdi 
 |-  ( k = l -> ( E. y e. U x = ( y .+ ( k .x. Z ) ) <-> E. z e. U x = ( z .+ ( l .x. Z ) ) ) )
30 29 cbvriotavw 
 |-  ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) = ( iota_ l e. K E. z e. U x = ( z .+ ( l .x. Z ) ) )
31 30 mpteq2i 
 |-  ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) ) = ( x e. V |-> ( iota_ l e. K E. z e. U x = ( z .+ ( l .x. Z ) ) ) )
32 15 31 eqtri 
 |-  G = ( x e. V |-> ( iota_ l e. K E. z e. U x = ( z .+ ( l .x. Z ) ) ) )
33 riotaex 
 |-  ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) e. _V
34 21 32 33 fvmpt 
 |-  ( X e. V -> ( G ` X ) = ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) )
35 dfsbcq 
 |-  ( ( G ` X ) = ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) -> ( [. ( G ` X ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) <-> [. ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) ) )
36 9 34 35 3syl 
 |-  ( ph -> ( [. ( G ` X ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) <-> [. ( iota_ l e. K E. z e. U X = ( z .+ ( l .x. Z ) ) ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) ) )
37 18 36 mpbird 
 |-  ( ph -> [. ( G ` X ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) )
38 fvex 
 |-  ( G ` X ) e. _V
39 oveq1 
 |-  ( l = ( G ` X ) -> ( l .x. Z ) = ( ( G ` X ) .x. Z ) )
40 39 oveq2d 
 |-  ( l = ( G ` X ) -> ( z .+ ( l .x. Z ) ) = ( z .+ ( ( G ` X ) .x. Z ) ) )
41 40 eqeq2d 
 |-  ( l = ( G ` X ) -> ( X = ( z .+ ( l .x. Z ) ) <-> X = ( z .+ ( ( G ` X ) .x. Z ) ) ) )
42 41 rexbidv 
 |-  ( l = ( G ` X ) -> ( E. z e. U X = ( z .+ ( l .x. Z ) ) <-> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) ) )
43 38 42 sbcie 
 |-  ( [. ( G ` X ) / l ]. E. z e. U X = ( z .+ ( l .x. Z ) ) <-> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) )
44 37 43 sylib 
 |-  ( ph -> E. z e. U X = ( z .+ ( ( G ` X ) .x. Z ) ) )