Metamath Proof Explorer

Theorem lshpsmreu

Description: Lemma for lshpkrex . Show uniqueness of ring multiplier k when a vector X is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv for a to c ? (Contributed by NM, 4-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lshpsmreu.v 
 |-  V = ( Base ` W )
2 lshpsmreu.a 
 |-  .+ = ( +g ` W )
3 lshpsmreu.n 
 |-  N = ( LSpan ` W )
4 lshpsmreu.p 
 |-  .(+) = ( LSSum ` W )
5 lshpsmreu.h 
 |-  H = ( LSHyp ` W )
6 lshpsmreu.w 
 |-  ( ph -> W e. LVec )
7 lshpsmreu.u 
 |-  ( ph -> U e. H )
8 lshpsmreu.z 
 |-  ( ph -> Z e. V )
9 lshpsmreu.x 
 |-  ( ph -> X e. V )
10 lshpsmreu.e 
 |-  ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
11 lshpsmreu.d 
 |-  D = ( Scalar ` W )
12 lshpsmreu.k 
 |-  K = ( Base ` D )
13 lshpsmreu.t 
 |-  .x. = ( .s ` W )
14 9 10 eleqtrrd 
 |-  ( ph -> X e. ( U .(+) ( N ` { Z } ) ) )
15 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
16 6 15 syl 
 |-  ( ph -> W e. LMod )
17 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
18 17 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
19 16 18 syl 
 |-  ( ph -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
20 17 5 16 7 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
21 19 20 sseldd 
 |-  ( ph -> U e. ( SubGrp ` W ) )
22 1 17 3 lspsncl 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
23 16 8 22 syl2anc 
 |-  ( ph -> ( N ` { Z } ) e. ( LSubSp ` W ) )
24 19 23 sseldd 
 |-  ( ph -> ( N ` { Z } ) e. ( SubGrp ` W ) )
25 2 4 lsmelval 
 |-  ( ( U e. ( SubGrp ` W ) /\ ( N ` { Z } ) e. ( SubGrp ` W ) ) -> ( X e. ( U .(+) ( N ` { Z } ) ) <-> E. c e. U E. z e. ( N ` { Z } ) X = ( c .+ z ) ) )
26 21 24 25 syl2anc 
 |-  ( ph -> ( X e. ( U .(+) ( N ` { Z } ) ) <-> E. c e. U E. z e. ( N ` { Z } ) X = ( c .+ z ) ) )
27 14 26 mpbid 
 |-  ( ph -> E. c e. U E. z e. ( N ` { Z } ) X = ( c .+ z ) )
28 df-rex 
 |-  ( E. z e. ( N ` { Z } ) X = ( c .+ z ) <-> E. z ( z e. ( N ` { Z } ) /\ X = ( c .+ z ) ) )
29 11 12 1 13 3 lspsnel 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( z e. ( N ` { Z } ) <-> E. b e. K z = ( b .x. Z ) ) )
30 16 8 29 syl2anc 
 |-  ( ph -> ( z e. ( N ` { Z } ) <-> E. b e. K z = ( b .x. Z ) ) )
31 30 anbi1d 
 |-  ( ph -> ( ( z e. ( N ` { Z } ) /\ X = ( c .+ z ) ) <-> ( E. b e. K z = ( b .x. Z ) /\ X = ( c .+ z ) ) ) )
32 r19.41v 
 |-  ( E. b e. K ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) <-> ( E. b e. K z = ( b .x. Z ) /\ X = ( c .+ z ) ) )
33 31 32 bitr4di 
 |-  ( ph -> ( ( z e. ( N ` { Z } ) /\ X = ( c .+ z ) ) <-> E. b e. K ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) ) )
34 33 exbidv 
 |-  ( ph -> ( E. z ( z e. ( N ` { Z } ) /\ X = ( c .+ z ) ) <-> E. z E. b e. K ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) ) )
35 rexcom4 
 |-  ( E. b e. K E. z ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) <-> E. z E. b e. K ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) )
36 ovex 
 |-  ( b .x. Z ) e. _V
37 oveq2 
 |-  ( z = ( b .x. Z ) -> ( c .+ z ) = ( c .+ ( b .x. Z ) ) )
38 37 eqeq2d 
 |-  ( z = ( b .x. Z ) -> ( X = ( c .+ z ) <-> X = ( c .+ ( b .x. Z ) ) ) )
39 36 38 ceqsexv 
 |-  ( E. z ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) <-> X = ( c .+ ( b .x. Z ) ) )
40 39 rexbii 
 |-  ( E. b e. K E. z ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) <-> E. b e. K X = ( c .+ ( b .x. Z ) ) )
41 35 40 bitr3i 
 |-  ( E. z E. b e. K ( z = ( b .x. Z ) /\ X = ( c .+ z ) ) <-> E. b e. K X = ( c .+ ( b .x. Z ) ) )
42 34 41 bitrdi 
 |-  ( ph -> ( E. z ( z e. ( N ` { Z } ) /\ X = ( c .+ z ) ) <-> E. b e. K X = ( c .+ ( b .x. Z ) ) ) )
43 28 42 syl5bb 
 |-  ( ph -> ( E. z e. ( N ` { Z } ) X = ( c .+ z ) <-> E. b e. K X = ( c .+ ( b .x. Z ) ) ) )
44 43 rexbidv 
 |-  ( ph -> ( E. c e. U E. z e. ( N ` { Z } ) X = ( c .+ z ) <-> E. c e. U E. b e. K X = ( c .+ ( b .x. Z ) ) ) )
45 27 44 mpbid 
 |-  ( ph -> E. c e. U E. b e. K X = ( c .+ ( b .x. Z ) ) )
46 rexcom 
 |-  ( E. c e. U E. b e. K X = ( c .+ ( b .x. Z ) ) <-> E. b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) )
47 45 46 sylib 
 |-  ( ph -> E. b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) )
48 oveq1 
 |-  ( c = a -> ( c .+ ( b .x. Z ) ) = ( a .+ ( b .x. Z ) ) )
49 48 eqeq2d 
 |-  ( c = a -> ( X = ( c .+ ( b .x. Z ) ) <-> X = ( a .+ ( b .x. Z ) ) ) )
50 49 cbvrexvw 
 |-  ( E. c e. U X = ( c .+ ( b .x. Z ) ) <-> E. a e. U X = ( a .+ ( b .x. Z ) ) )
51 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
52 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
53 simp11l 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ph )
54 53 21 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> U e. ( SubGrp ` W ) )
55 53 24 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( N ` { Z } ) e. ( SubGrp ` W ) )
56 1 51 3 4 5 6 7 8 10 lshpdisj 
 |-  ( ph -> ( U i^i ( N ` { Z } ) ) = { ( 0g ` W ) } )
57 53 56 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( U i^i ( N ` { Z } ) ) = { ( 0g ` W ) } )
58 53 6 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> W e. LVec )
59 58 15 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> W e. LMod )
60 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
61 59 60 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> W e. Abel )
62 52 61 54 55 ablcntzd 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> U C_ ( ( Cntz ` W ) ` ( N ` { Z } ) ) )
63 simp12 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> a e. U )
64 simp2 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> c e. U )
65 simp1rl 
 |-  ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) -> b e. K )
66 65 3ad2ant1 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> b e. K )
67 53 8 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> Z e. V )
68 1 13 11 12 3 59 66 67 lspsneli 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( b .x. Z ) e. ( N ` { Z } ) )
69 simp1rr 
 |-  ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) -> l e. K )
70 69 3ad2ant1 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> l e. K )
71 1 13 11 12 3 59 70 67 lspsneli 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( l .x. Z ) e. ( N ` { Z } ) )
72 simp13 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> X = ( a .+ ( b .x. Z ) ) )
73 simp3 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> X = ( c .+ ( l .x. Z ) ) )
74 72 73 eqtr3d 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( a .+ ( b .x. Z ) ) = ( c .+ ( l .x. Z ) ) )
75 2 51 52 54 55 57 62 63 64 68 71 74 subgdisj2 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( b .x. Z ) = ( l .x. Z ) )
76 53 7 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> U e. H )
77 53 10 syl 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( U .(+) ( N ` { Z } ) ) = V )
78 1 3 4 5 51 59 76 67 77 lshpne0 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> Z =/= ( 0g ` W ) )
79 1 13 11 12 51 58 66 70 67 78 lvecvscan2 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> ( ( b .x. Z ) = ( l .x. Z ) <-> b = l ) )
80 75 79 mpbid 
 |-  ( ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) /\ c e. U /\ X = ( c .+ ( l .x. Z ) ) ) -> b = l )
81 80 rexlimdv3a 
 |-  ( ( ( ph /\ ( b e. K /\ l e. K ) ) /\ a e. U /\ X = ( a .+ ( b .x. Z ) ) ) -> ( E. c e. U X = ( c .+ ( l .x. Z ) ) -> b = l ) )
82 81 rexlimdv3a 
 |-  ( ( ph /\ ( b e. K /\ l e. K ) ) -> ( E. a e. U X = ( a .+ ( b .x. Z ) ) -> ( E. c e. U X = ( c .+ ( l .x. Z ) ) -> b = l ) ) )
83 50 82 syl5bi 
 |-  ( ( ph /\ ( b e. K /\ l e. K ) ) -> ( E. c e. U X = ( c .+ ( b .x. Z ) ) -> ( E. c e. U X = ( c .+ ( l .x. Z ) ) -> b = l ) ) )
84 83 impd 
 |-  ( ( ph /\ ( b e. K /\ l e. K ) ) -> ( ( E. c e. U X = ( c .+ ( b .x. Z ) ) /\ E. c e. U X = ( c .+ ( l .x. Z ) ) ) -> b = l ) )
85 84 ralrimivva 
 |-  ( ph -> A. b e. K A. l e. K ( ( E. c e. U X = ( c .+ ( b .x. Z ) ) /\ E. c e. U X = ( c .+ ( l .x. Z ) ) ) -> b = l ) )
86 oveq1 
 |-  ( b = l -> ( b .x. Z ) = ( l .x. Z ) )
87 86 oveq2d 
 |-  ( b = l -> ( c .+ ( b .x. Z ) ) = ( c .+ ( l .x. Z ) ) )
88 87 eqeq2d 
 |-  ( b = l -> ( X = ( c .+ ( b .x. Z ) ) <-> X = ( c .+ ( l .x. Z ) ) ) )
89 88 rexbidv 
 |-  ( b = l -> ( E. c e. U X = ( c .+ ( b .x. Z ) ) <-> E. c e. U X = ( c .+ ( l .x. Z ) ) ) )
90 89 reu4 
 |-  ( E! b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) <-> ( E. b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) /\ A. b e. K A. l e. K ( ( E. c e. U X = ( c .+ ( b .x. Z ) ) /\ E. c e. U X = ( c .+ ( l .x. Z ) ) ) -> b = l ) ) )
91 47 85 90 sylanbrc 
 |-  ( ph -> E! b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) )
92 oveq1 
 |-  ( b = k -> ( b .x. Z ) = ( k .x. Z ) )
93 92 oveq2d 
 |-  ( b = k -> ( c .+ ( b .x. Z ) ) = ( c .+ ( k .x. Z ) ) )
94 93 eqeq2d 
 |-  ( b = k -> ( X = ( c .+ ( b .x. Z ) ) <-> X = ( c .+ ( k .x. Z ) ) ) )
95 94 rexbidv 
 |-  ( b = k -> ( E. c e. U X = ( c .+ ( b .x. Z ) ) <-> E. c e. U X = ( c .+ ( k .x. Z ) ) ) )
96 95 cbvreuvw 
 |-  ( E! b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) <-> E! k e. K E. c e. U X = ( c .+ ( k .x. Z ) ) )
97 oveq1 
 |-  ( c = y -> ( c .+ ( k .x. Z ) ) = ( y .+ ( k .x. Z ) ) )
98 97 eqeq2d 
 |-  ( c = y -> ( X = ( c .+ ( k .x. Z ) ) <-> X = ( y .+ ( k .x. Z ) ) ) )
99 98 cbvrexvw 
 |-  ( E. c e. U X = ( c .+ ( k .x. Z ) ) <-> E. y e. U X = ( y .+ ( k .x. Z ) ) )
100 99 reubii 
 |-  ( E! k e. K E. c e. U X = ( c .+ ( k .x. Z ) ) <-> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )
101 96 100 bitri 
 |-  ( E! b e. K E. c e. U X = ( c .+ ( b .x. Z ) ) <-> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )
102 91 101 sylib 
 |-  ( ph -> E! k e. K E. y e. U X = ( y .+ ( k .x. Z ) ) )