Metamath Proof Explorer

Theorem iscom2

Description: A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

Ref Expression
Assertion iscom2 
|- ( ( G e. A /\ H e. B ) -> ( <. G , H >. e. Com2 <-> A. a e. ran G A. b e. ran G ( a H b ) = ( b H a ) ) )

Proof

Step Hyp Ref Expression
1 df-com2 
 |-  Com2 = { <. x , y >. | A. a e. ran x A. b e. ran x ( a y b ) = ( b y a ) }
2 1 a1i 
 |-  ( ( G e. A /\ H e. B ) -> Com2 = { <. x , y >. | A. a e. ran x A. b e. ran x ( a y b ) = ( b y a ) } )
3 2 eleq2d 
 |-  ( ( G e. A /\ H e. B ) -> ( <. G , H >. e. Com2 <-> <. G , H >. e. { <. x , y >. | A. a e. ran x A. b e. ran x ( a y b ) = ( b y a ) } ) )
4 rneq 
 |-  ( x = G -> ran x = ran G )
5 4 raleqdv 
 |-  ( x = G -> ( A. b e. ran x ( a y b ) = ( b y a ) <-> A. b e. ran G ( a y b ) = ( b y a ) ) )
6 4 5 raleqbidv 
 |-  ( x = G -> ( A. a e. ran x A. b e. ran x ( a y b ) = ( b y a ) <-> A. a e. ran G A. b e. ran G ( a y b ) = ( b y a ) ) )
7 oveq 
 |-  ( y = H -> ( a y b ) = ( a H b ) )
8 oveq 
 |-  ( y = H -> ( b y a ) = ( b H a ) )
9 7 8 eqeq12d 
 |-  ( y = H -> ( ( a y b ) = ( b y a ) <-> ( a H b ) = ( b H a ) ) )
10 9 2ralbidv 
 |-  ( y = H -> ( A. a e. ran G A. b e. ran G ( a y b ) = ( b y a ) <-> A. a e. ran G A. b e. ran G ( a H b ) = ( b H a ) ) )
11 6 10 opelopabg 
 |-  ( ( G e. A /\ H e. B ) -> ( <. G , H >. e. { <. x , y >. | A. a e. ran x A. b e. ran x ( a y b ) = ( b y a ) } <-> A. a e. ran G A. b e. ran G ( a H b ) = ( b H a ) ) )
12 3 11 bitrd 
 |-  ( ( G e. A /\ H e. B ) -> ( <. G , H >. e. Com2 <-> A. a e. ran G A. b e. ran G ( a H b ) = ( b H a ) ) )