Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  svli2 Unicode version

Theorem svli2 25484
Description: If a finite sequence of vectors  U ( k ) are linearly independant, two combinations of those vectors are equal iff the scalars are equal. (Contributed by FL, 9-Nov-2010.)
Hypotheses
Ref Expression
svli2.1  |-  X  =  ran  + t
svli2.2  |-  0 t  =  (GId `  + t )
svli2.7  |-  + t  =  ( 1st `  ( 1st `  R ) )
svli2.3  |-  . t  =  ( 2nd `  ( 1st `  R ) )
svli2.4  |-  0 w  =  (GId `  + w )
svli2.5  |-  + w  =  ( 1st `  ( 2nd `  R ) )
svli2.6  |-  W  =  ran  + w
svli2.8  |-  . w  =  ( 2nd `  ( 2nd `  R ) )
Assertion
Ref Expression
svli2  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  = 
prod_ k  e.  (
1 ... N ) + w ( S 2 . w U )  <->  A. k  e.  ( 1 ... N
) S1  =  S 2 ) )
Distinct variable groups:    k, + t, s    k, + w,
s    k, . t    s, . w    s, 0 t    k, 0 w, s    k, N, s    R, k    s, S1    s, S 2    U, s    k, W    k, X, s
Allowed substitution hints:    R( s)    U( k)    W( s)    S1( k)    S 2( k)    . t(
s)    0 t( k)    . w( k)

Proof of Theorem svli2
StepHypRef Expression
1 simp11 985 . . 3  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  ->  R  e.  Vec  )
2 elnnuz 10264 . . . . . . . . 9  |-  ( N  e.  NN  <->  N  e.  ( ZZ>= `  1 )
)
32biimpi 186 . . . . . . . 8  |-  ( N  e.  NN  ->  N  e.  ( ZZ>= `  1 )
)
433ad2ant3 978 . . . . . . 7  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  N  e.  ( ZZ>= `  1 )
)
54adantr 451 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  N  e.  ( ZZ>= ` 
1 ) )
6 svli2.5 . . . . . . . . 9  |-  + w  =  ( 1st `  ( 2nd `  R ) )
76vecax1 25453 . . . . . . . 8  |-  ( R  e.  Vec  ->  + w  e.  AbelOp )
873ad2ant1 976 . . . . . . 7  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  + w  e.  AbelOp )
98adantr 451 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  + w  e.  AbelOp )
10 r19.26 2675 . . . . . . . . . . 11  |-  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S1  e.  X )  <->  ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X ) )
11 svli2.8 . . . . . . . . . . . . . . . . . 18  |-  . w  =  ( 2nd `  ( 2nd `  R ) )
12 svli2.6 . . . . . . . . . . . . . . . . . 18  |-  W  =  ran  + w
13 svli2.1 . . . . . . . . . . . . . . . . . 18  |-  X  =  ran  + t
14 svli2.7 . . . . . . . . . . . . . . . . . 18  |-  + t  =  ( 1st `  ( 1st `  R ) )
156, 11, 12, 13, 14prodvs 25468 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Vec  /\  S1  e.  X  /\  U  e.  W )  ->  ( S1 . w U )  e.  W )
16153exp 1150 . . . . . . . . . . . . . . . 16  |-  ( R  e.  Vec  ->  ( S1  e.  X  ->  ( U  e.  W  ->  (
S1 . w U
)  e.  W ) ) )
1716com13 74 . . . . . . . . . . . . . . 15  |-  ( U  e.  W  ->  ( S1  e.  X  ->  ( R  e.  Vec  ->  ( S1 . w U )  e.  W ) ) )
1817imp 418 . . . . . . . . . . . . . 14  |-  ( ( U  e.  W  /\  S1  e.  X )  -> 
( R  e.  Vec  ->  ( S1 . w U )  e.  W
) )
1918com12 27 . . . . . . . . . . . . 13  |-  ( R  e.  Vec  ->  (
( U  e.  W  /\  S1  e.  X )  ->  ( S1 . w U )  e.  W
) )
2019ralimdv 2622 . . . . . . . . . . . 12  |-  ( R  e.  Vec  ->  ( A. k  e.  (
1 ... N ) ( U  e.  W  /\  S1  e.  X )  ->  A. k  e.  (
1 ... N ) (
S1 . w U
)  e.  W ) )
2120com12 27 . . . . . . . . . . 11  |-  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S1  e.  X )  -> 
( R  e.  Vec  ->  A. k  e.  ( 1 ... N ) ( S1 . w U )  e.  W
) )
2210, 21sylbir 204 . . . . . . . . . 10  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X )  ->  ( R  e.  Vec  ->  A. k  e.  ( 1 ... N
) ( S1 . w U )  e.  W
) )
23223adant3 975 . . . . . . . . 9  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  ( R  e.  Vec  ->  A. k  e.  ( 1 ... N
) ( S1 . w U )  e.  W
) )
2423com12 27 . . . . . . . 8  |-  ( R  e.  Vec  ->  (
( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  ->  A. k  e.  ( 1 ... N ) ( S1 . w U )  e.  W
) )
25243ad2ant1 976 . . . . . . 7  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( S1 . w U )  e.  W
) )
2625imp 418 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  A. k  e.  (
1 ... N ) (
S1 . w U
)  e.  W )
2712clfsebs5 25382 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
1 )  /\  + w  e.  AbelOp  /\  A. k  e.  ( 1 ... N ) (
S1 . w U
)  e.  W )  ->  prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  e.  W )
285, 9, 26, 27syl3anc 1182 . . . . 5  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  e.  W
)
29 r19.26 2675 . . . . . . . . . . 11  |-  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S 2  e.  X
)  <->  ( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N ) S 2  e.  X
) )
306, 11, 12, 13, 14prodvs 25468 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Vec  /\  S 2  e.  X  /\  U  e.  W
)  ->  ( S 2 . w U )  e.  W )
31303exp 1150 . . . . . . . . . . . . . . . 16  |-  ( R  e.  Vec  ->  ( S 2  e.  X  ->  ( U  e.  W  ->  ( S 2 . w U )  e.  W
) ) )
3231com13 74 . . . . . . . . . . . . . . 15  |-  ( U  e.  W  ->  ( S 2  e.  X  ->  ( R  e.  Vec  ->  ( S 2 . w U )  e.  W
) ) )
3332imp 418 . . . . . . . . . . . . . 14  |-  ( ( U  e.  W  /\  S 2  e.  X
)  ->  ( R  e.  Vec  ->  ( S 2 . w U )  e.  W ) )
3433com12 27 . . . . . . . . . . . . 13  |-  ( R  e.  Vec  ->  (
( U  e.  W  /\  S 2  e.  X
)  ->  ( S 2 . w U )  e.  W ) )
3534ralimdv 2622 . . . . . . . . . . . 12  |-  ( R  e.  Vec  ->  ( A. k  e.  (
1 ... N ) ( U  e.  W  /\  S 2  e.  X
)  ->  A. k  e.  ( 1 ... N
) ( S 2 . w U )  e.  W ) )
3635com12 27 . . . . . . . . . . 11  |-  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S 2  e.  X
)  ->  ( R  e.  Vec  ->  A. k  e.  ( 1 ... N
) ( S 2 . w U )  e.  W ) )
3729, 36sylbir 204 . . . . . . . . . 10  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  ->  ( R  e. 
Vec  ->  A. k  e.  ( 1 ... N ) ( S 2 . w U )  e.  W
) )
38373adant2 974 . . . . . . . . 9  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  ( R  e.  Vec  ->  A. k  e.  ( 1 ... N
) ( S 2 . w U )  e.  W ) )
3938com12 27 . . . . . . . 8  |-  ( R  e.  Vec  ->  (
( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  ->  A. k  e.  ( 1 ... N ) ( S 2 . w U )  e.  W
) )
40393ad2ant1 976 . . . . . . 7  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( S 2 . w U )  e.  W ) )
4140imp 418 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  A. k  e.  (
1 ... N ) ( S 2 . w U )  e.  W
)
4212clfsebs5 25382 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
1 )  /\  + w  e.  AbelOp  /\  A. k  e.  ( 1 ... N ) ( S 2 . w U )  e.  W
)  ->  prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
)  e.  W )
435, 9, 41, 42syl3anc 1182 . . . . 5  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  prod_ k  e.  ( 1 ... N ) + w ( S 2 . w U )  e.  W )
4428, 43jca 518 . . . 4  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  e.  W  /\  prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
)  e.  W ) )
45443adant3 975 . . 3  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  e.  W  /\  prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
)  e.  W ) )
46 svli2.4 . . . 4  |-  0 w  =  (GId `  + w )
47 eqid 2283 . . . 4  |-  (  /g  `  + w )  =  (  /g  `  + w )
4846, 6, 47, 12mvecrtol 25473 . . 3  |-  ( ( R  e.  Vec  /\  ( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  e.  W  /\  prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
)  e.  W ) )  ->  ( prod_ k  e.  ( 1 ... N ) + w
( S1 . w U
)  =  prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
)  <->  ( prod_ k  e.  ( 1 ... N
) + w ( S1 . w U ) (  /g  `  + w ) prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
) )  =  0 w ) )
491, 45, 48syl2anc 642 . 2  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  = 
prod_ k  e.  (
1 ... N ) + w ( S 2 . w U )  <->  ( prod_ k  e.  ( 1 ... N ) + w
( S1 . w U
) (  /g  `  + w ) prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
) )  =  0 w ) )
50 r19.26 2675 . . . . . . 7  |-  ( A. k  e.  ( 1 ... N ) ( ( S1 . w U )  e.  W  /\  ( S 2 . w U )  e.  W
)  <->  ( A. k  e.  ( 1 ... N
) ( S1 . w U )  e.  W  /\  A. k  e.  ( 1 ... N ) ( S 2 . w U )  e.  W
) )
5126, 41, 50sylanbrc 645 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  A. k  e.  (
1 ... N ) ( ( S1 . w U )  e.  W  /\  ( S 2 . w U )  e.  W
) )
525, 51, 93jca 1132 . . . . 5  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  -> 
( N  e.  (
ZZ>= `  1 )  /\  A. k  e.  ( 1 ... N ) ( ( S1 . w U )  e.  W  /\  ( S 2 . w U )  e.  W
)  /\  + w  e.  AbelOp ) )
53523adant3 975 . . . 4  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( N  e.  (
ZZ>= `  1 )  /\  A. k  e.  ( 1 ... N ) ( ( S1 . w U )  e.  W  /\  ( S 2 . w U )  e.  W
)  /\  + w  e.  AbelOp ) )
5412, 47fprodsub 25379 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
1 )  /\  A. k  e.  ( 1 ... N ) ( ( S1 . w U )  e.  W  /\  ( S 2 . w U )  e.  W
)  /\  + w  e.  AbelOp )  ->  prod_ k  e.  ( 1 ... N ) + w ( (
S1 . w U
) (  /g  `  + w ) ( S 2 . w U
) )  =  (
prod_ k  e.  (
1 ... N ) + w ( S1 . w U ) (  /g  `  + w ) prod_
k  e.  ( 1 ... N ) + w ( S 2 . w U ) ) )
5554eqcomd 2288 . . . 4  |-  ( ( N  e.  ( ZZ>= ` 
1 )  /\  A. k  e.  ( 1 ... N ) ( ( S1 . w U )  e.  W  /\  ( S 2 . w U )  e.  W
)  /\  + w  e.  AbelOp )  ->  ( prod_ k  e.  ( 1 ... N
) + w ( S1 . w U ) (  /g  `  + w ) prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
) )  =  prod_ k  e.  ( 1 ... N ) + w
( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) ) )
5653, 55syl 15 . . 3  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U ) (  /g  `  + w
) prod_ k  e.  ( 1 ... N ) + w ( S 2 . w U
) )  =  prod_ k  e.  ( 1 ... N ) + w
( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) ) )
5756eqeq1d 2291 . 2  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( ( prod_ k  e.  ( 1 ... N
) + w ( S1 . w U ) (  /g  `  + w ) prod_ k  e.  ( 1 ... N
) + w ( S 2 . w U
) )  =  0 w  <->  prod_ k  e.  ( 1 ... N ) + w ( (
S1 . w U
) (  /g  `  + w ) ( S 2 . w U
) )  =  0 w ) )
58 r19.26-3 2677 . . . . . . . 8  |-  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  <->  ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )
59 eqid 2283 . . . . . . . . . . . . . 14  |-  (  /g  `  + t )  =  (  /g  `  + t )
60 svli2.3 . . . . . . . . . . . . . 14  |-  . t  =  ( 2nd `  ( 1st `  R ) )
6113, 14, 59, 6, 47, 11, 12, 60vecax5c 25483 . . . . . . . . . . . . 13  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps )  ->  (
( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X
)  ->  ( ( S1 (  /g  `  + t ) S 2
) . w U
)  =  ( (
S1 . w U
) (  /g  `  + w ) ( S 2 . w U
) ) ) )
62613adant3 975 . . . . . . . . . . . 12  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  ( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  ( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) ) ) )
6362imp 418 . . . . . . . . . . 11  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )
)  ->  ( ( S1 (  /g  `  + t ) S 2
) . w U
)  =  ( (
S1 . w U
) (  /g  `  + w ) ( S 2 . w U
) ) )
6463eqcomd 2288 . . . . . . . . . 10  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )
)  ->  ( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U
) )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U ) )
6564ex 423 . . . . . . . . 9  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  ( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U ) ) )
6665ralimdv 2622 . . . . . . . 8  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  A. k  e.  ( 1 ... N ) ( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U ) ) )
6758, 66syl5bir 209 . . . . . . 7  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( ( S1 . w U ) (  /g  `  + w
) ( S 2 . w U ) )  =  ( ( S1 (  /g  `  + t
) S 2 ) . w U ) ) )
6867imp 418 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  A. k  e.  (
1 ... N ) ( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U ) )
69683adant3 975 . . . . 5  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  ->  A. k  e.  (
1 ... N ) ( ( S1 . w U ) (  /g  `  + w ) ( S 2 . w U ) )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U ) )
7069prodeq3d 25315 . . . 4  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  ->  prod_ k  e.  ( 1 ... N ) + w ( ( S1 . w U ) (  /g  `  + w
) ( S 2 . w U ) )  =  prod_ k  e.  ( 1 ... N ) + w ( (
S1 (  /g  `  + t ) S 2
) . w U
) )
7170eqeq1d 2291 . . 3  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( (
S1 . w U
) (  /g  `  + w ) ( S 2 . w U
) )  =  0 w  <->  prod_ k  e.  ( 1 ... N ) + w ( (
S1 (  /g  `  + t ) S 2
) . w U
)  =  0 w
) )
72 fvex 5539 . . . . . . . . . . . . . 14  |-  ( 1st `  ( 1st `  R
) )  e.  _V
7314, 72eqeltri 2353 . . . . . . . . . . . . 13  |-  + t  e.  _V
74 fvex 5539 . . . . . . . . . . . . . 14  |-  ( 2nd `  ( 1st `  R
) )  e.  _V
7560, 74eqeltri 2353 . . . . . . . . . . . . 13  |-  . t  e.  _V
7673, 75op1st 6128 . . . . . . . . . . . 12  |-  ( 1st `  <. + t ,  . t >. )  =  + t
7776eqcomi 2287 . . . . . . . . . . 11  |-  + t  =  ( 1st `  <. + t ,  . t >. )
7877rngogrpo 21057 . . . . . . . . . 10  |-  ( <. + t ,  . t >.  e.  RingOps  ->  + t  e.  GrpOp
)
79 r19.26 2675 . . . . . . . . . . . 12  |-  ( A. k  e.  ( 1 ... N ) (
S1  e.  X  /\  S 2  e.  X
)  <->  ( A. k  e.  ( 1 ... N
) S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X
) )
8013, 59grpodivcl 20914 . . . . . . . . . . . . . . 15  |-  ( ( + t  e.  GrpOp  /\  S1  e.  X  /\  S 2  e.  X )  ->  ( S1 (  /g  `  + t ) S 2 )  e.  X
)
81803expib 1154 . . . . . . . . . . . . . 14  |-  ( + t  e.  GrpOp  ->  (
( S1  e.  X  /\  S 2  e.  X
)  ->  ( S1 (  /g  `  + t
) S 2 )  e.  X ) )
8281ralimdv 2622 . . . . . . . . . . . . 13  |-  ( + t  e.  GrpOp  ->  ( A. k  e.  (
1 ... N ) (
S1  e.  X  /\  S 2  e.  X
)  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  e.  X
) )
8382com12 27 . . . . . . . . . . . 12  |-  ( A. k  e.  ( 1 ... N ) (
S1  e.  X  /\  S 2  e.  X
)  ->  ( + t  e.  GrpOp  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  e.  X
) )
8479, 83sylbir 204 . . . . . . . . . . 11  |-  ( ( A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  ->  ( + t  e.  GrpOp  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  e.  X
) )
85843adant1 973 . . . . . . . . . 10  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  ( + t  e.  GrpOp  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  e.  X
) )
8678, 85syl5com 26 . . . . . . . . 9  |-  ( <. + t ,  . t >.  e.  RingOps  ->  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  e.  X
) )
87863ad2ant2 977 . . . . . . . 8  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  e.  X
) )
8887imp 418 . . . . . . 7  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  A. k  e.  (
1 ... N ) (
S1 (  /g  `  + t ) S 2
)  e.  X )
89 eqid 2283 . . . . . . . 8  |-  ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
)  =  ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
)
9089fmpt 5681 . . . . . . 7  |-  ( A. k  e.  ( 1 ... N ) (
S1 (  /g  `  + t ) S 2
)  e.  X  <->  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) : ( 1 ... N
) --> X )
9188, 90sylib 188 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  -> 
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) ) : ( 1 ... N
) --> X )
9273rnex 4942 . . . . . . . 8  |-  ran  + t  e.  _V
9313, 92eqeltri 2353 . . . . . . 7  |-  X  e. 
_V
94 ovex 5883 . . . . . . 7  |-  ( 1 ... N )  e. 
_V
9593, 94elmap 6796 . . . . . 6  |-  ( ( k  e.  ( 1 ... N )  |->  (
S1 (  /g  `  + t ) S 2
) )  e.  ( X  ^m  ( 1 ... N ) )  <-> 
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) ) : ( 1 ... N
) --> X )
9691, 95sylibr 203 . . . . 5  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  -> 
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )
97963adant3 975 . . . 4  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )
98 nfmpt1 4109 . . . . . . . . . . . . . 14  |-  F/_ k
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )
9998nfeq2 2430 . . . . . . . . . . . . 13  |-  F/ k  s  =  ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
)
100 fveq1 5524 . . . . . . . . . . . . . . 15  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( s `  k
)  =  ( ( k  e.  ( 1 ... N )  |->  (
S1 (  /g  `  + t ) S 2
) ) `  k
) )
101100oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( ( s `  k ) . w U )  =  ( ( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U ) )
102101a1d 22 . . . . . . . . . . . . 13  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( k  e.  ( 1 ... N )  ->  ( ( s `
 k ) . w U )  =  ( ( ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
) `  k ) . w U ) ) )
10399, 102ralrimi 2624 . . . . . . . . . . . 12  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  ->  A. k  e.  (
1 ... N ) ( ( s `  k
) . w U
)  =  ( ( ( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U ) )
104103prodeq3d 25315 . . . . . . . . . . 11  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  ->  prod_ k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  = 
prod_ k  e.  (
1 ... N ) + w ( ( ( k  e.  ( 1 ... N )  |->  (
S1 (  /g  `  + t ) S 2
) ) `  k
) . w U
) )
105104eqeq1d 2291 . . . . . . . . . 10  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( ( s `  k ) . w U )  =  0 w  <->  prod_ k  e.  ( 1 ... N
) + w (
( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U )  =  0 w ) )
106100eqeq1d 2291 . . . . . . . . . . 11  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( ( s `  k )  =  0 t  <->  ( ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
) `  k )  =  0 t )
)
10799, 106ralbid 2561 . . . . . . . . . 10  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t  <->  A. k  e.  ( 1 ... N ) ( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k )  =  0 t ) )
108105, 107imbi12d 311 . . . . . . . . 9  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( ( prod_ k  e.  ( 1 ... N
) + w (
( s `  k
) . w U
)  =  0 w  ->  A. k  e.  ( 1 ... N ) ( s `  k
)  =  0 t
)  <->  ( prod_ k  e.  ( 1 ... N
) + w (
( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
) `  k )  =  0 t )
) )
109 prodeq3 25309 . . . . . . . . . . . 12  |-  ( A. k  e.  ( 1 ... N ) ( ( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U )  ->  prod_ k  e.  ( 1 ... N ) + w
( ( ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
) `  k ) . w U )  = 
prod_ k  e.  (
1 ... N ) + w ( ( S1 (  /g  `  + t
) S 2 ) . w U ) )
110 ovex 5883 . . . . . . . . . . . . . 14  |-  ( S1 (  /g  `  + t
) S 2 )  e.  _V
11189fvmpt2 5608 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( 1 ... N )  /\  ( S1 (  /g  `  + t ) S 2
)  e.  _V )  ->  ( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k )  =  (
S1 (  /g  `  + t ) S 2
) )
112110, 111mpan2 652 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... N )  ->  (
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) ) `  k )  =  (
S1 (  /g  `  + t ) S 2
) )
113112oveq1d 5873 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... N )  ->  (
( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U )  =  ( ( S1 (  /g  `  + t ) S 2 ) . w U ) )
114109, 113mprg 2612 . . . . . . . . . . 11  |-  prod_ k  e.  ( 1 ... N
) + w (
( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k ) . w U )  =  prod_ k  e.  ( 1 ... N ) + w
( ( S1 (  /g  `  + t ) S 2 ) . w U )
115114eqeq1i 2290 . . . . . . . . . 10  |-  ( prod_
k  e.  ( 1 ... N ) + w ( ( ( k  e.  ( 1 ... N )  |->  (
S1 (  /g  `  + t ) S 2
) ) `  k
) . w U
)  =  0 w  <->  prod_
k  e.  ( 1 ... N ) + w ( ( S1 (  /g  `  + t
) S 2 ) . w U )  =  0 w )
116112eqeq1d 2291 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  (
( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k )  =  0 t  <->  ( S1 (  /g  `  + t ) S 2 )  =  0 t ) )
117116ralbiia 2575 . . . . . . . . . 10  |-  ( A. k  e.  ( 1 ... N ) ( ( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) ) `  k )  =  0 t  <->  A. k  e.  ( 1 ... N ) ( S1 (  /g  `  + t ) S 2 )  =  0 t )
118115, 117imbi12i 316 . . . . . . . . 9  |-  ( (
prod_ k  e.  (
1 ... N ) + w ( ( ( k  e.  ( 1 ... N )  |->  (
S1 (  /g  `  + t ) S 2
) ) `  k
) . w U
)  =  0 w  ->  A. k  e.  ( 1 ... N ) ( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) ) `  k )  =  0 t )  <->  ( prod_ k  e.  ( 1 ... N ) + w
( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t ) )
119108, 118syl6bb 252 . . . . . . . 8  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( ( prod_ k  e.  ( 1 ... N
) + w (
( s `  k
) . w U
)  =  0 w  ->  A. k  e.  ( 1 ... N ) ( s `  k
)  =  0 t
)  <->  ( prod_ k  e.  ( 1 ... N
) + w (
( S1 (  /g  `  + t ) S 2
) . w U
)  =  0 w  ->  A. k  e.  ( 1 ... N ) ( S1 (  /g  `  + t ) S 2 )  =  0 t ) ) )
120119rspccv 2881 . . . . . . 7  |-  ( A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t )  ->  (
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) )  ->  ( prod_ k  e.  ( 1 ... N
) + w (
( S1 (  /g  `  + t ) S 2
) . w U
)  =  0 w  ->  A. k  e.  ( 1 ... N ) ( S1 (  /g  `  + t ) S 2 )  =  0 t ) ) )
1211203ad2ant3 978 . . . . . 6  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) )  ->  ( prod_ k  e.  ( 1 ... N
) + w (
( S1 (  /g  `  + t ) S 2
) . w U
)  =  0 w  ->  A. k  e.  ( 1 ... N ) ( S1 (  /g  `  + t ) S 2 )  =  0 t ) ) )
122121imp 418 . . . . 5  |-  ( ( ( ( R  e. 
Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  /\  A. s  e.  ( X  ^m  (
1 ... N ) ) ( prod_ k  e.  ( 1 ... N ) + w ( ( s `  k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N ) ( s `  k )  =  0 t )
)  /\  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  ->  ( prod_ k  e.  ( 1 ... N ) + w
( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t ) )
123 oveq1 5865 . . . . . . . . . 10  |-  ( (
S1 (  /g  `  + t ) S 2
)  =  0 t  ->  ( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  ( 0 t . w U ) )
124123ralimi 2618 . . . . . . . . 9  |-  ( A. k  e.  ( 1 ... N ) (
S1 (  /g  `  + t ) S 2
)  =  0 t  ->  A. k  e.  ( 1 ... N ) ( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  ( 0 t . w U ) )
125124prodeq3d 25315 . . . . . . . 8  |-  ( A. k  e.  ( 1 ... N ) (
S1 (  /g  `  + t ) S 2
)  =  0 t  ->  prod_ k  e.  ( 1 ... N ) + w ( (
S1 (  /g  `  + t ) S 2
) . w U
)  =  prod_ k  e.  ( 1 ... N
) + w (
0 t . w U ) )
126125adantl 452 . . . . . . 7  |-  ( ( ( ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  /\  ( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  /\  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t )  ->  prod_ k  e.  ( 1 ... N ) + w
( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  prod_ k  e.  ( 1 ... N ) + w
( 0 t . w U ) )
1276rneqi 4905 . . . . . . . . . . . . . . . . . . 19  |-  ran  + w  =  ran  ( 1st `  ( 2nd `  R
) )
12812, 127eqtri 2303 . . . . . . . . . . . . . . . . . 18  |-  W  =  ran  ( 1st `  ( 2nd `  R ) )
129 svli2.2 . . . . . . . . . . . . . . . . . 18  |-  0 t  =  (GId `  + t )
1306fveq2i 5528 . . . . . . . . . . . . . . . . . . 19  |-  (GId `  + w )  =  (GId
`  ( 1st `  ( 2nd `  R ) ) )
13146, 130eqtri 2303 . . . . . . . . . . . . . . . . . 18  |-  0 w  =  (GId `  ( 1st `  ( 2nd `  R
) ) )
132128, 129, 14, 60, 11, 131mulveczer 25479 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  U  e.  W )  ->  (
0 t . w U )  =  0 w )
1331323expia 1153 . . . . . . . . . . . . . . . 16  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps )  ->  ( U  e.  W  ->  ( 0 t . w U )  =  0 w ) )
134133ralimdv 2622 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps )  ->  ( A. k  e.  (
1 ... N ) U  e.  W  ->  A. k  e.  ( 1 ... N
) ( 0 t . w U )  =  0 w ) )
135134com12 27 . . . . . . . . . . . . . 14  |-  ( A. k  e.  ( 1 ... N ) U  e.  W  ->  (
( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps )  ->  A. k  e.  (
1 ... N ) ( 0 t . w U )  =  0 w ) )
1361353ad2ant1 976 . . . . . . . . . . . . 13  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  (
( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps )  ->  A. k  e.  (
1 ... N ) ( 0 t . w U )  =  0 w ) )
137136com12 27 . . . . . . . . . . . 12  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps )  ->  (
( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  ->  A. k  e.  ( 1 ... N ) ( 0 t . w U )  =  0 w ) )
1381373adant3 975 . . . . . . . . . . 11  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( 0 t . w U )  =  0 w ) )
139138imp 418 . . . . . . . . . 10  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  A. k  e.  (
1 ... N ) ( 0 t . w U )  =  0 w )
140139prodeq3d 25315 . . . . . . . . 9  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  ->  prod_ k  e.  ( 1 ... N ) + w ( 0 t . w U )  = 
prod_ k  e.  (
1 ... N ) + w 0 w )
1411403adant3 975 . . . . . . . 8  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  ->  prod_ k  e.  ( 1 ... N ) + w ( 0 t . w U )  = 
prod_ k  e.  (
1 ... N ) + w 0 w )
142141ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  /\  ( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  /\  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t )  ->  prod_ k  e.  ( 1 ... N ) + w
( 0 t . w U )  =  prod_ k  e.  ( 1 ... N ) + w
0 w )
143 ablogrpo 20951 . . . . . . . . . . . . 13  |-  ( + w  e.  AbelOp  ->  + w  e.  GrpOp )
144 grpomndo 21013 . . . . . . . . . . . . 13  |-  ( + w  e.  GrpOp  ->  + w  e. MndOp )
145143, 144syl 15 . . . . . . . . . . . 12  |-  ( + w  e.  AbelOp  ->  + w  e. MndOp )
146 mndomgmid 21009 . . . . . . . . . . . 12  |-  ( + w  e. MndOp  ->  + w  e.  ( Magma  i^i  ExId  )
)
1477, 145, 1463syl 18 . . . . . . . . . . 11  |-  ( R  e.  Vec  ->  + w  e.  ( Magma  i^i  ExId  )
)
1481473ad2ant1 976 . . . . . . . . . 10  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  + w  e.  ( Magma  i^i  ExId  )
)
14946fincmpzer 25350 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
1 )  /\  + w  e.  ( Magma  i^i 
ExId  ) )  ->  prod_ k  e.  ( 1 ... N ) + w 0 w  =  0 w )
1504, 148, 149syl2anc 642 . . . . . . . . 9  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  prod_ k  e.  ( 1 ... N
) + w 0 w  =  0 w
)
1511503ad2ant1 976 . . . . . . . 8  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  ->  prod_ k  e.  ( 1 ... N ) + w 0 w  =  0 w )
152151ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  /\  ( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  /\  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t )  ->  prod_ k  e.  ( 1 ... N ) + w
0 w  =  0 w )
153126, 142, 1523eqtrd 2319 . . . . . 6  |-  ( ( ( ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  /\  ( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  /\  A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t )  ->  prod_ k  e.  ( 1 ... N ) + w
( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  0 w )
154153ex 423 . . . . 5  |-  ( ( ( ( R  e. 
Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  /\  A. s  e.  ( X  ^m  (
1 ... N ) ) ( prod_ k  e.  ( 1 ... N ) + w ( ( s `  k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N ) ( s `  k )  =  0 t )
)  /\  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  ->  ( A. k  e.  ( 1 ... N ) (
S1 (  /g  `  + t ) S 2
)  =  0 t  ->  prod_ k  e.  ( 1 ... N ) + w ( (
S1 (  /g  `  + t ) S 2
) . w U
)  =  0 w
) )
155122, 154impbid 183 . . . 4  |-  ( ( ( ( R  e. 
Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  ( 1 ... N
) U  e.  W  /\  A. k  e.  ( 1 ... N )
S1  e.  X  /\  A. k  e.  ( 1 ... N ) S 2  e.  X )  /\  A. s  e.  ( X  ^m  (
1 ... N ) ) ( prod_ k  e.  ( 1 ... N ) + w ( ( s `  k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N ) ( s `  k )  =  0 t )
)  /\  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  e.  ( X  ^m  (
1 ... N ) ) )  ->  ( prod_ k  e.  ( 1 ... N ) + w
( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  0 w  <->  A. k  e.  ( 1 ... N ) ( S1 (  /g  `  + t ) S 2 )  =  0 t ) )
15697, 155mpdan 649 . . 3  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( (
S1 (  /g  `  + t ) S 2
) . w U
)  =  0 w  <->  A. k  e.  ( 1 ... N ) (
S1 (  /g  `  + t ) S 2
)  =  0 t
) )
15713, 129, 59grpodivzer 25377 . . . . . . . . . . . . . . 15  |-  ( ( + t  e.  GrpOp  /\  S1  e.  X  /\  S 2  e.  X )  ->  ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
) )
1581573exp 1150 . . . . . . . . . . . . . 14  |-  ( + t  e.  GrpOp  ->  ( S1  e.  X  ->  ( S 2  e.  X  ->  ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
) ) ) )
159158com3l 75 . . . . . . . . . . . . 13  |-  ( S1  e.  X  ->  ( S 2  e.  X  -> 
( + t  e.  GrpOp  ->  ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
) ) ) )
160159imp 418 . . . . . . . . . . . 12  |-  ( (
S1  e.  X  /\  S 2  e.  X
)  ->  ( + t  e.  GrpOp  ->  (
( S1 (  /g  `  + t ) S 2
)  =  0 t  <->  S1  =  S 2 )
) )
1611603adant1 973 . . . . . . . . . . 11  |-  ( ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  ( + t  e.  GrpOp  ->  ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
) ) )
162161com12 27 . . . . . . . . . 10  |-  ( + t  e.  GrpOp  ->  (
( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X
)  ->  ( ( S1 (  /g  `  + t ) S 2
)  =  0 t  <->  S1  =  S 2 )
) )
163162ralimdv 2622 . . . . . . . . 9  |-  ( + t  e.  GrpOp  ->  ( A. k  e.  (
1 ... N ) ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  A. k  e.  ( 1 ... N ) ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
) ) )
16478, 163syl 15 . . . . . . . 8  |-  ( <. + t ,  . t >.  e.  RingOps  ->  ( A. k  e.  ( 1 ... N
) ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  A. k  e.  ( 1 ... N
) ( ( S1 (  /g  `  + t
) S 2 )  =  0 t  <->  S1  =  S 2 ) ) )
1651643ad2ant2 977 . . . . . . 7  |-  ( ( R  e.  Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  A. k  e.  ( 1 ... N ) ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
) ) )
166 ralbi 2679 . . . . . . 7  |-  ( A. k  e.  ( 1 ... N ) ( ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  S1  =  S 2
)  ->  ( A. k  e.  ( 1 ... N ) (
S1 (  /g  `  + t ) S 2
)  =  0 t  <->  A. k  e.  ( 1 ... N ) S1  =  S 2 ) )
167165, 166syl6com 31 . . . . . 6  |-  ( A. k  e.  ( 1 ... N ) ( U  e.  W  /\  S1  e.  X  /\  S 2  e.  X )  ->  ( ( R  e. 
Vec  /\  <. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  A. k  e.  ( 1 ... N )
S1  =  S 2
) ) )
16858, 167sylbir 204 . . . . 5  |-  ( ( A. k  e.  ( 1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  ->  (
( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  ->  ( A. k  e.  (
1 ... N ) (
S1 (  /g  `  + t ) S 2
)  =  0 t  <->  A. k  e.  ( 1 ... N ) S1  =  S 2 ) ) )
169168impcom 419 . . . 4  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X ) )  -> 
( A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  A. k  e.  ( 1 ... N )
S1  =  S 2
) )
1701693adant3 975 . . 3  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( A. k  e.  ( 1 ... N
) ( S1 (  /g  `  + t ) S 2 )  =  0 t  <->  A. k  e.  ( 1 ... N )
S1  =  S 2
) )
17171, 156, 1703bitrd 270 . 2  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( (
S1 . w U
) (  /g  `  + w ) ( S 2 . w U
) )  =  0 w  <->  A. k  e.  ( 1 ... N )
S1  =  S 2
) )
17249, 57, 1713bitrd 270 1  |-  ( ( ( R  e.  Vec  /\ 
<. + t ,  . t >.  e.  RingOps  /\  N  e.  NN )  /\  ( A. k  e.  (
1 ... N ) U  e.  W  /\  A. k  e.  ( 1 ... N ) S1  e.  X  /\  A. k  e.  ( 1 ... N
) S 2  e.  X )  /\  A. s  e.  ( X  ^m  ( 1 ... N
) ) ( prod_
k  e.  ( 1 ... N ) + w ( ( s `
 k ) . w U )  =  0 w  ->  A. k  e.  ( 1 ... N
) ( s `  k )  =  0 t ) )  -> 
( prod_ k  e.  ( 1 ... N ) + w ( S1 . w U )  = 
prod_ k  e.  (
1 ... N ) + w ( S 2 . w U )  <->  A. k  e.  ( 1 ... N
) S1  =  S 2 ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   _Vcvv 2788    i^i cin 3151   <.cop 3643    e. cmpt 4077   ran crn 4690   -->wf 5251   ` cfv 5255  (class class class)co 5858   1stc1st 6120   2ndc2nd 6121    ^m cmap 6772   1c1 8738   NNcn 9746   ZZ>=cuz 10230   ...cfz 10782   GrpOpcgr 20853  GIdcgi 20854    /g cgs 20856   AbelOpcablo 20948    ExId cexid 20981   Magmacmagm 20985  MndOpcmndo 21004   RingOpscrngo 21042   prod_cprd 25298    Vec cvec 25449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-fzo 10871  df-seq 11047  df-grpo 20858  df-gid 20859  df-ginv 20860  df-gdiv 20861  df-ablo 20949  df-ass 20980  df-exid 20982  df-mgm 20986  df-sgr 20998  df-mndo 21005  df-rngo 21043  df-prod 25299  df-vec 25450
  Copyright terms: Public domain W3C validator