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

Theorem svli2 25587
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 10280 . . . . . . . . 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 25556 . . . . . . . 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 2688 . . . . . . . . . . 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 25571 . . . . . . . . . . . . . . . . 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 2635 . . . . . . . . . . . 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 25485 . . . . . 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 2688 . . . . . . . . . . 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 25571 . . . . . . . . . . . . . . . . 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 2635 . . . . . . . . . . . 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 25485 . . . . . 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 2296 . . . 4  |-  (  /g  `  + w )  =  (  /g  `  + w )
4846, 6, 47, 12mvecrtol 25576 . . 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 2688 . . . . . . 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 25482 . . . . 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 2301 . . . 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 2304 . 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 2690 . . . . . . . 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 2296 . . . . . . . . . . . . . 14  |-  (  /g  `  + t )  =  (  /g  `  + t )
60 svli2.3 . . . . . . . . . . . . . 14  |-  . t  =  ( 2nd `  ( 1st `  R ) )
6113, 14, 59, 6, 47, 11, 12, 60vecax5c 25586 . . . . . . . . . . . . 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 2301 . . . . . . . . . 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 2635 . . . . . . . 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 25418 . . . 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 2304 . . 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 5555 . . . . . . . . . . . . . 14  |-  ( 1st `  ( 1st `  R
) )  e.  _V
7314, 72eqeltri 2366 . . . . . . . . . . . . 13  |-  + t  e.  _V
74 fvex 5555 . . . . . . . . . . . . . 14  |-  ( 2nd `  ( 1st `  R
) )  e.  _V
7560, 74eqeltri 2366 . . . . . . . . . . . . 13  |-  . t  e.  _V
7673, 75op1st 6144 . . . . . . . . . . . 12  |-  ( 1st `  <. + t ,  . t >. )  =  + t
7776eqcomi 2300 . . . . . . . . . . 11  |-  + t  =  ( 1st `  <. + t ,  . t >. )
7877rngogrpo 21073 . . . . . . . . . 10  |-  ( <. + t ,  . t >.  e.  RingOps  ->  + t  e.  GrpOp
)
79 r19.26 2688 . . . . . . . . . . . 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 20930 . . . . . . . . . . . . . . 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 2635 . . . . . . . . . . . . 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 2296 . . . . . . . 8  |-  ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
)  =  ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
)
9089fmpt 5697 . . . . . . 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 4958 . . . . . . . 8  |-  ran  + t  e.  _V
9313, 92eqeltri 2366 . . . . . . 7  |-  X  e. 
_V
94 ovex 5899 . . . . . . 7  |-  ( 1 ... N )  e. 
_V
9593, 94elmap 6812 . . . . . 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 4125 . . . . . . . . . . . . . 14  |-  F/_ k
( k  e.  ( 1 ... N ) 
|->  ( S1 (  /g  `  + t ) S 2 ) )
9998nfeq2 2443 . . . . . . . . . . . . 13  |-  F/ k  s  =  ( k  e.  ( 1 ... N )  |->  ( S1 (  /g  `  + t
) S 2 )
)
100 fveq1 5540 . . . . . . . . . . . . . . 15  |-  ( s  =  ( k  e.  ( 1 ... N
)  |->  ( S1 (  /g  `  + t ) S 2 ) )  -> 
( s `  k
)  =  ( ( k  e.  ( 1 ... N )  |->  (
S1 (  /g  `  + t ) S 2
) ) `  k
) )
101100oveq1d 5889 . . . . . . . . . . . . . 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 2637 . . . . . . . . . . . 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 25418 . . . . . . . . . . 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 2304 . . . . . . . . . 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 2304 . . . . . . . . . . 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 2574 . . . . . . . . . 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 25412 . . . . . . . . . . . 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 5899 . . . . . . . . . . . . . 14  |-  ( S1 (  /g  `  + t
) S 2 )  e.  _V
11189fvmpt2 5624 . . . . . . . . . . . . . 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 5889 . . . . . . . . . . . 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 2625 . . . . . . . . . . 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 2303 . . . . . . . . . 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 2304 . . . . . . . . . . 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 2588 . . . . . . . . . 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 2894 . . . . . . 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 5881 . . . . . . . . . 10  |-  ( (
S1 (  /g  `  + t ) S 2
)  =  0 t  ->  ( ( S1 (  /g  `  + t ) S 2 ) . w U )  =  ( 0 t . w U ) )
124123ralimi 2631 . . . . . . . . 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 25418 . . . . . . . 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 4921 . . . . . . . . . . . . . . . . . . 19  |-  ran  + w  =  ran  ( 1st `  ( 2nd `  R
) )
12812, 127eqtri 2316 . . . . . . . . . . . . . . . . . 18  |-  W  =  ran  ( 1st `  ( 2nd `  R ) )
129 svli2.2 . . . . . . . . . . . . . . . . . 18  |-  0 t  =  (GId `  + t )
1306fveq2i 5544 . . . . . . . . . . . . . . . . . . 19  |-  (GId `  + w )  =  (GId
`  ( 1st `  ( 2nd `  R ) ) )
13146, 130eqtri 2316 . . . . . . . . . . . . . . . . . 18  |-  0 w  =  (GId `  ( 1st `  ( 2nd `  R
) ) )
132128, 129, 14, 60, 11, 131mulveczer 25582 . . . . . . . . . . . . . . . . 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 2635 . . . . . . . . . . . . . . 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 25418 . . . . . . . . 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 20967 . . . . . . . . . . . . 13  |-  ( + w  e.  AbelOp  ->  + w  e.  GrpOp )
144 grpomndo 21029 . . . . . . . . . . . . 13  |-  ( + w  e.  GrpOp  ->  + w  e. MndOp )
145143, 144syl 15 . . . . . . . . . . . 12  |-  ( + w  e.  AbelOp  ->  + w  e. MndOp )
146 mndomgmid 21025 . . . . . . . . . . . 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 25453 . . . . . . . . . 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 2332 . . . . . 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 25480 . . . . . . . . . . . . . . 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 2635 . . . . . . . . 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 2692 . . . . . . 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 1632    e. wcel 1696   A.wral 2556   _Vcvv 2801    i^i cin 3164   <.cop 3656    e. cmpt 4093   ran crn 4706   -->wf 5267   ` cfv 5271  (class class class)co 5874   1stc1st 6136   2ndc2nd 6137    ^m cmap 6788   1c1 8754   NNcn 9762   ZZ>=cuz 10246   ...cfz 10798   GrpOpcgr 20869  GIdcgi 20870    /g cgs 20872   AbelOpcablo 20964    ExId cexid 20997   Magmacmagm 21001  MndOpcmndo 21020   RingOpscrngo 21058   prod_cprd 25401    Vec cvec 25552
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830
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 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-er 6676  df-map 6790  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-nn 9763  df-n0 9982  df-z 10041  df-uz 10247  df-fz 10799  df-fzo 10887  df-seq 11063  df-grpo 20874  df-gid 20875  df-ginv 20876  df-gdiv 20877  df-ablo 20965  df-ass 20996  df-exid 20998  df-mgm 21002  df-sgr 21014  df-mndo 21021  df-rngo 21059  df-prod 25402  df-vec 25553
  Copyright terms: Public domain W3C validator