This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isvclem

Description: Lemma for isvcOLD . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Hypothesis isvclem.1 
|- X = ran G
Assertion isvclem 
|- ( ( G e. _V /\ S e. _V ) -> ( <. G , S >. e. CVecOLD <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isvclem.1 
 |-  X = ran G
2 df-vc 
 |-  CVecOLD = { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) }
3 2 eleq2i 
 |-  ( <. G , S >. e. CVecOLD <-> <. G , S >. e. { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) } )
4 eleq1 
 |-  ( g = G -> ( g e. AbelOp <-> G e. AbelOp ) )
5 rneq 
 |-  ( g = G -> ran g = ran G )
6 5 1 eqtr4di 
 |-  ( g = G -> ran g = X )
7 xpeq2 
 |-  ( ran g = X -> ( CC X. ran g ) = ( CC X. X ) )
8 7 feq2d 
 |-  ( ran g = X -> ( s : ( CC X. ran g ) --> ran g <-> s : ( CC X. X ) --> ran g ) )
9 feq3 
 |-  ( ran g = X -> ( s : ( CC X. X ) --> ran g <-> s : ( CC X. X ) --> X ) )
10 8 9 bitrd 
 |-  ( ran g = X -> ( s : ( CC X. ran g ) --> ran g <-> s : ( CC X. X ) --> X ) )
11 6 10 syl 
 |-  ( g = G -> ( s : ( CC X. ran g ) --> ran g <-> s : ( CC X. X ) --> X ) )
12 oveq 
 |-  ( g = G -> ( x g z ) = ( x G z ) )
13 12 oveq2d 
 |-  ( g = G -> ( y s ( x g z ) ) = ( y s ( x G z ) ) )
14 oveq 
 |-  ( g = G -> ( ( y s x ) g ( y s z ) ) = ( ( y s x ) G ( y s z ) ) )
15 13 14 eqeq12d 
 |-  ( g = G -> ( ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) <-> ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) ) )
16 6 15 raleqbidv 
 |-  ( g = G -> ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) <-> A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) ) )
17 oveq 
 |-  ( g = G -> ( ( y s x ) g ( z s x ) ) = ( ( y s x ) G ( z s x ) ) )
18 17 eqeq2d 
 |-  ( g = G -> ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) <-> ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) ) )
19 18 anbi1d 
 |-  ( g = G -> ( ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) <-> ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) )
20 19 ralbidv 
 |-  ( g = G -> ( A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) <-> A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) )
21 16 20 anbi12d 
 |-  ( g = G -> ( ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) )
22 21 ralbidv 
 |-  ( g = G -> ( A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) )
23 22 anbi2d 
 |-  ( g = G -> ( ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) )
24 6 23 raleqbidv 
 |-  ( g = G -> ( A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) )
25 4 11 24 3anbi123d 
 |-  ( g = G -> ( ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) <-> ( G e. AbelOp /\ s : ( CC X. X ) --> X /\ A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) ) )
26 feq1 
 |-  ( s = S -> ( s : ( CC X. X ) --> X <-> S : ( CC X. X ) --> X ) )
27 oveq 
 |-  ( s = S -> ( 1 s x ) = ( 1 S x ) )
28 27 eqeq1d 
 |-  ( s = S -> ( ( 1 s x ) = x <-> ( 1 S x ) = x ) )
29 oveq 
 |-  ( s = S -> ( y s ( x G z ) ) = ( y S ( x G z ) ) )
30 oveq 
 |-  ( s = S -> ( y s x ) = ( y S x ) )
31 oveq 
 |-  ( s = S -> ( y s z ) = ( y S z ) )
32 30 31 oveq12d 
 |-  ( s = S -> ( ( y s x ) G ( y s z ) ) = ( ( y S x ) G ( y S z ) ) )
33 29 32 eqeq12d 
 |-  ( s = S -> ( ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) <-> ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) ) )
34 33 ralbidv 
 |-  ( s = S -> ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) <-> A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) ) )
35 oveq 
 |-  ( s = S -> ( ( y + z ) s x ) = ( ( y + z ) S x ) )
36 oveq 
 |-  ( s = S -> ( z s x ) = ( z S x ) )
37 30 36 oveq12d 
 |-  ( s = S -> ( ( y s x ) G ( z s x ) ) = ( ( y S x ) G ( z S x ) ) )
38 35 37 eqeq12d 
 |-  ( s = S -> ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) <-> ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) ) )
39 oveq 
 |-  ( s = S -> ( ( y x. z ) s x ) = ( ( y x. z ) S x ) )
40 oveq 
 |-  ( s = S -> ( y s ( z s x ) ) = ( y S ( z s x ) ) )
41 36 oveq2d 
 |-  ( s = S -> ( y S ( z s x ) ) = ( y S ( z S x ) ) )
42 40 41 eqtrd 
 |-  ( s = S -> ( y s ( z s x ) ) = ( y S ( z S x ) ) )
43 39 42 eqeq12d 
 |-  ( s = S -> ( ( ( y x. z ) s x ) = ( y s ( z s x ) ) <-> ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) )
44 38 43 anbi12d 
 |-  ( s = S -> ( ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) <-> ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) )
45 44 ralbidv 
 |-  ( s = S -> ( A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) <-> A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) )
46 34 45 anbi12d 
 |-  ( s = S -> ( ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) )
47 46 ralbidv 
 |-  ( s = S -> ( A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) )
48 28 47 anbi12d 
 |-  ( s = S -> ( ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
49 48 ralbidv 
 |-  ( s = S -> ( A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
50 26 49 3anbi23d 
 |-  ( s = S -> ( ( G e. AbelOp /\ s : ( CC X. X ) --> X /\ A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )
51 25 50 opelopabg 
 |-  ( ( G e. _V /\ S e. _V ) -> ( <. G , S >. e. { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) } <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )
52 3 51 bitrid 
 |-  ( ( G e. _V /\ S e. _V ) -> ( <. G , S >. e. CVecOLD <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )