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
srngcl.b B = Base R
srngmul.t · ˙ = R
Assertion srngmul R *-Ring X B Y B ˙ X · ˙ Y = ˙ Y · ˙ ˙ X

Proof

Step Hyp Ref Expression
1 srngcl.i ˙ = * R
2 srngcl.b B = Base R
3 srngmul.t · ˙ = R
4 eqid opp r R = opp r R
5 eqid 𝑟𝑓 R = 𝑟𝑓 R
6 4 5 srngrhm R *-Ring 𝑟𝑓 R R RingHom opp r R
7 eqid opp r R = opp r R
8 2 3 7 rhmmul 𝑟𝑓 R R RingHom opp r R X B Y B 𝑟𝑓 R X · ˙ Y = 𝑟𝑓 R X opp r R 𝑟𝑓 R Y
9 6 8 syl3an1 R *-Ring X B Y B 𝑟𝑓 R X · ˙ Y = 𝑟𝑓 R X opp r R 𝑟𝑓 R Y
10 2 3 4 7 opprmul 𝑟𝑓 R X opp r R 𝑟𝑓 R Y = 𝑟𝑓 R Y · ˙ 𝑟𝑓 R X
11 9 10 syl6eq R *-Ring X B Y B 𝑟𝑓 R X · ˙ Y = 𝑟𝑓 R Y · ˙ 𝑟𝑓 R X
12 srngring R *-Ring R Ring
13 2 3 ringcl R Ring X B Y B X · ˙ Y B
14 12 13 syl3an1 R *-Ring X B Y B X · ˙ Y B
15 2 1 5 stafval X · ˙ Y B 𝑟𝑓 R X · ˙ Y = ˙ X · ˙ Y
16 14 15 syl R *-Ring X B Y B 𝑟𝑓 R X · ˙ Y = ˙ X · ˙ Y
17 2 1 5 stafval Y B 𝑟𝑓 R Y = ˙ Y
18 17 3ad2ant3 R *-Ring X B Y B 𝑟𝑓 R Y = ˙ Y
19 2 1 5 stafval X B 𝑟𝑓 R X = ˙ X
20 19 3ad2ant2 R *-Ring X B Y B 𝑟𝑓 R X = ˙ X
21 18 20 oveq12d R *-Ring X B Y B 𝑟𝑓 R Y · ˙ 𝑟𝑓 R X = ˙ Y · ˙ ˙ X
22 11 16 21 3eqtr3d R *-Ring X B Y B ˙ X · ˙ Y = ˙ Y · ˙ ˙ X