Metamath Proof Explorer

Theorem lshpkrlem1

Description: Lemma for lshpkrex . The value of tentative functional G is zero iff its argument belongs to hyperplane U . (Contributed by NM, 14-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 lshpkrlem1 
|- ( ph -> ( X e. U <-> ( G ` X ) = .0. ) )

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 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
17 6 16 syl 
 |-  ( ph -> W e. LMod )
18 11 lmodfgrp 
 |-  ( W e. LMod -> D e. Grp )
19 12 14 grpidcl 
 |-  ( D e. Grp -> .0. e. K )
20 17 18 19 3syl 
 |-  ( ph -> .0. e. K )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 lshpsmreu 
 |-  ( ph -> E! k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) )
22 oveq1 
 |-  ( k = .0. -> ( k .x. Z ) = ( .0. .x. Z ) )
23 22 oveq2d 
 |-  ( k = .0. -> ( b .+ ( k .x. Z ) ) = ( b .+ ( .0. .x. Z ) ) )
24 23 eqeq2d 
 |-  ( k = .0. -> ( X = ( b .+ ( k .x. Z ) ) <-> X = ( b .+ ( .0. .x. Z ) ) ) )
25 24 rexbidv 
 |-  ( k = .0. -> ( E. b e. U X = ( b .+ ( k .x. Z ) ) <-> E. b e. U X = ( b .+ ( .0. .x. Z ) ) ) )
26 25 riota2 
 |-  ( ( .0. e. K /\ E! k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) ) -> ( E. b e. U X = ( b .+ ( .0. .x. Z ) ) <-> ( iota_ k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) ) = .0. ) )
27 20 21 26 syl2anc 
 |-  ( ph -> ( E. b e. U X = ( b .+ ( .0. .x. Z ) ) <-> ( iota_ k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) ) = .0. ) )
28 simpr 
 |-  ( ( ph /\ X e. U ) -> X e. U )
29 eqidd 
 |-  ( ( ph /\ X e. U ) -> X = X )
30 eqeq2 
 |-  ( b = X -> ( X = b <-> X = X ) )
31 30 rspcev 
 |-  ( ( X e. U /\ X = X ) -> E. b e. U X = b )
32 28 29 31 syl2anc 
 |-  ( ( ph /\ X e. U ) -> E. b e. U X = b )
33 32 ex 
 |-  ( ph -> ( X e. U -> E. b e. U X = b ) )
34 eleq1a 
 |-  ( b e. U -> ( X = b -> X e. U ) )
35 34 a1i 
 |-  ( ph -> ( b e. U -> ( X = b -> X e. U ) ) )
36 35 rexlimdv 
 |-  ( ph -> ( E. b e. U X = b -> X e. U ) )
37 33 36 impbid 
 |-  ( ph -> ( X e. U <-> E. b e. U X = b ) )
38 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
39 1 11 13 14 38 lmod0vs 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( .0. .x. Z ) = ( 0g ` W ) )
40 17 8 39 syl2anc 
 |-  ( ph -> ( .0. .x. Z ) = ( 0g ` W ) )
41 40 adantr 
 |-  ( ( ph /\ b e. U ) -> ( .0. .x. Z ) = ( 0g ` W ) )
42 41 oveq2d 
 |-  ( ( ph /\ b e. U ) -> ( b .+ ( .0. .x. Z ) ) = ( b .+ ( 0g ` W ) ) )
43 6 adantr 
 |-  ( ( ph /\ b e. U ) -> W e. LVec )
44 43 16 syl 
 |-  ( ( ph /\ b e. U ) -> W e. LMod )
45 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
46 45 5 17 7 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
47 1 45 lssel 
 |-  ( ( U e. ( LSubSp ` W ) /\ b e. U ) -> b e. V )
48 46 47 sylan 
 |-  ( ( ph /\ b e. U ) -> b e. V )
49 1 2 38 lmod0vrid 
 |-  ( ( W e. LMod /\ b e. V ) -> ( b .+ ( 0g ` W ) ) = b )
50 44 48 49 syl2anc 
 |-  ( ( ph /\ b e. U ) -> ( b .+ ( 0g ` W ) ) = b )
51 42 50 eqtrd 
 |-  ( ( ph /\ b e. U ) -> ( b .+ ( .0. .x. Z ) ) = b )
52 51 eqeq2d 
 |-  ( ( ph /\ b e. U ) -> ( X = ( b .+ ( .0. .x. Z ) ) <-> X = b ) )
53 52 bicomd 
 |-  ( ( ph /\ b e. U ) -> ( X = b <-> X = ( b .+ ( .0. .x. Z ) ) ) )
54 53 rexbidva 
 |-  ( ph -> ( E. b e. U X = b <-> E. b e. U X = ( b .+ ( .0. .x. Z ) ) ) )
55 37 54 bitrd 
 |-  ( ph -> ( X e. U <-> E. b e. U X = ( b .+ ( .0. .x. Z ) ) ) )
56 eqeq1 
 |-  ( x = X -> ( x = ( y .+ ( k .x. Z ) ) <-> X = ( y .+ ( k .x. Z ) ) ) )
57 56 rexbidv 
 |-  ( x = X -> ( E. y e. U x = ( y .+ ( k .x. Z ) ) <-> E. y e. U X = ( y .+ ( k .x. Z ) ) ) )
58 57 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 ) ) ) )
59 riotaex 
 |-  ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) e. _V
60 58 15 59 fvmpt 
 |-  ( X e. V -> ( G ` X ) = ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) )
61 oveq1 
 |-  ( y = b -> ( y .+ ( k .x. Z ) ) = ( b .+ ( k .x. Z ) ) )
62 61 eqeq2d 
 |-  ( y = b -> ( X = ( y .+ ( k .x. Z ) ) <-> X = ( b .+ ( k .x. Z ) ) ) )
63 62 cbvrexvw 
 |-  ( E. y e. U X = ( y .+ ( k .x. Z ) ) <-> E. b e. U X = ( b .+ ( k .x. Z ) ) )
64 63 a1i 
 |-  ( k e. K -> ( E. y e. U X = ( y .+ ( k .x. Z ) ) <-> E. b e. U X = ( b .+ ( k .x. Z ) ) ) )
65 64 riotabiia 
 |-  ( iota_ k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) ) = ( iota_ k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) )
66 60 65 eqtrdi 
 |-  ( X e. V -> ( G ` X ) = ( iota_ k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) ) )
67 9 66 syl 
 |-  ( ph -> ( G ` X ) = ( iota_ k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) ) )
68 67 eqeq1d 
 |-  ( ph -> ( ( G ` X ) = .0. <-> ( iota_ k e. K E. b e. U X = ( b .+ ( k .x. Z ) ) ) = .0. ) )
69 27 55 68 3bitr4d 
 |-  ( ph -> ( X e. U <-> ( G ` X ) = .0. ) )