Metamath Proof Explorer

Theorem srngmul

Description: The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srngcl.i 
|- .* = ( *r ` R )
srngcl.b 
|- B = ( Base ` R )
srngmul.t 
|- .x. = ( .r ` R )
Assertion srngmul 
|- ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .x. Y ) ) = ( ( .* ` Y ) .x. ( .* ` X ) ) )

Proof

Step Hyp Ref Expression
1 srngcl.i 
 |-  .* = ( *r ` R )
2 srngcl.b 
 |-  B = ( Base ` R )
3 srngmul.t 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
5 eqid 
 |-  ( *rf ` R ) = ( *rf ` R )
6 4 5 srngrhm 
 |-  ( R e. *Ring -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )
7 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
8 2 3 7 rhmmul 
 |-  ( ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .x. Y ) ) = ( ( ( *rf ` R ) ` X ) ( .r ` ( oppR ` R ) ) ( ( *rf ` R ) ` Y ) ) )
9 6 8 syl3an1 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .x. Y ) ) = ( ( ( *rf ` R ) ` X ) ( .r ` ( oppR ` R ) ) ( ( *rf ` R ) ` Y ) ) )
10 2 3 4 7 opprmul 
 |-  ( ( ( *rf ` R ) ` X ) ( .r ` ( oppR ` R ) ) ( ( *rf ` R ) ` Y ) ) = ( ( ( *rf ` R ) ` Y ) .x. ( ( *rf ` R ) ` X ) )
11 9 10 eqtrdi 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .x. Y ) ) = ( ( ( *rf ` R ) ` Y ) .x. ( ( *rf ` R ) ` X ) ) )
12 srngring 
 |-  ( R e. *Ring -> R e. Ring )
13 2 3 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
14 12 13 syl3an1 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
15 2 1 5 stafval 
 |-  ( ( X .x. Y ) e. B -> ( ( *rf ` R ) ` ( X .x. Y ) ) = ( .* ` ( X .x. Y ) ) )
16 14 15 syl 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .x. Y ) ) = ( .* ` ( X .x. Y ) ) )
17 2 1 5 stafval 
 |-  ( Y e. B -> ( ( *rf ` R ) ` Y ) = ( .* ` Y ) )
18 17 3ad2ant3 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` Y ) = ( .* ` Y ) )
19 2 1 5 stafval 
 |-  ( X e. B -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
20 19 3ad2ant2 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
21 18 20 oveq12d 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( ( *rf ` R ) ` Y ) .x. ( ( *rf ` R ) ` X ) ) = ( ( .* ` Y ) .x. ( .* ` X ) ) )
22 11 16 21 3eqtr3d 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .x. Y ) ) = ( ( .* ` Y ) .x. ( .* ` X ) ) )