# 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 ) ) )`