# 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 = ( *𝑟𝑅 )
srngcl.b 𝐵 = ( Base ‘ 𝑅 )
srngmul.t · = ( .r𝑅 )
Assertion srngmul ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑌 ) · ( 𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 srngcl.i = ( *𝑟𝑅 )
2 srngcl.b 𝐵 = ( Base ‘ 𝑅 )
3 srngmul.t · = ( .r𝑅 )
4 eqid ( oppr𝑅 ) = ( oppr𝑅 )
5 eqid ( *rf𝑅 ) = ( *rf𝑅 )
6 4 5 srngrhm ( 𝑅 ∈ *-Ring → ( *rf𝑅 ) ∈ ( 𝑅 RingHom ( oppr𝑅 ) ) )
7 eqid ( .r ‘ ( oppr𝑅 ) ) = ( .r ‘ ( oppr𝑅 ) )
8 2 3 7 rhmmul ( ( ( *rf𝑅 ) ∈ ( 𝑅 RingHom ( oppr𝑅 ) ) ∧ 𝑋𝐵𝑌𝐵 ) → ( ( *rf𝑅 ) ‘ ( 𝑋 · 𝑌 ) ) = ( ( ( *rf𝑅 ) ‘ 𝑋 ) ( .r ‘ ( oppr𝑅 ) ) ( ( *rf𝑅 ) ‘ 𝑌 ) ) )
9 6 8 syl3an1 ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ( *rf𝑅 ) ‘ ( 𝑋 · 𝑌 ) ) = ( ( ( *rf𝑅 ) ‘ 𝑋 ) ( .r ‘ ( oppr𝑅 ) ) ( ( *rf𝑅 ) ‘ 𝑌 ) ) )
10 2 3 4 7 opprmul ( ( ( *rf𝑅 ) ‘ 𝑋 ) ( .r ‘ ( oppr𝑅 ) ) ( ( *rf𝑅 ) ‘ 𝑌 ) ) = ( ( ( *rf𝑅 ) ‘ 𝑌 ) · ( ( *rf𝑅 ) ‘ 𝑋 ) )
11 9 10 eqtrdi ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ( *rf𝑅 ) ‘ ( 𝑋 · 𝑌 ) ) = ( ( ( *rf𝑅 ) ‘ 𝑌 ) · ( ( *rf𝑅 ) ‘ 𝑋 ) ) )
12 srngring ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )
13 2 3 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
14 12 13 syl3an1 ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
15 2 1 5 stafval ( ( 𝑋 · 𝑌 ) ∈ 𝐵 → ( ( *rf𝑅 ) ‘ ( 𝑋 · 𝑌 ) ) = ( ‘ ( 𝑋 · 𝑌 ) ) )
16 14 15 syl ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ( *rf𝑅 ) ‘ ( 𝑋 · 𝑌 ) ) = ( ‘ ( 𝑋 · 𝑌 ) ) )
17 2 1 5 stafval ( 𝑌𝐵 → ( ( *rf𝑅 ) ‘ 𝑌 ) = ( 𝑌 ) )
18 17 3ad2ant3 ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ( *rf𝑅 ) ‘ 𝑌 ) = ( 𝑌 ) )
19 2 1 5 stafval ( 𝑋𝐵 → ( ( *rf𝑅 ) ‘ 𝑋 ) = ( 𝑋 ) )
20 19 3ad2ant2 ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ( *rf𝑅 ) ‘ 𝑋 ) = ( 𝑋 ) )
21 18 20 oveq12d ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ( ( *rf𝑅 ) ‘ 𝑌 ) · ( ( *rf𝑅 ) ‘ 𝑋 ) ) = ( ( 𝑌 ) · ( 𝑋 ) ) )
22 11 16 21 3eqtr3d ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑌 ) · ( 𝑋 ) ) )