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	$⊢ \underset{˙}{} = _{R}$
	srngcl.b	$⊢ B = {Base}_{R}$
	srngmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	srngmul	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to \underset{˙}{} (X \underset{˙}{\cdot} Y) = \underset{˙}{} (Y) \underset{˙}{\cdot} \underset{˙}{} (X)$

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	$⊢ \underset{˙}{} = _{R}$
2		srngcl.b	$⊢ B = {Base}_{R}$
3		srngmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
5		eqid	$⊢ _{𝑟𝑓} (R) = _{𝑟𝑓} (R)$
6	4 5	srngrhm	$⊢ R \in -Ring \to _{𝑟𝑓} (R) \in (R RingHom {opp}_{r} (R))$
7		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
8	2 3 7	rhmmul	$⊢ (_{𝑟𝑓} (R) \in (R RingHom {opp}_{r} (R)) \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{\cdot} Y) = _{𝑟𝑓} (R) (X) \cdot_{{opp}_{r} (R)} _{𝑟𝑓} (R) (Y)$
9	6 8	syl3an1	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{\cdot} Y) = _{𝑟𝑓} (R) (X) \cdot_{{opp}_{r} (R)} _{𝑟𝑓} (R) (Y)$
10	2 3 4 7	opprmul	$⊢ _{𝑟𝑓} (R) (X) \cdot_{{opp}_{r} (R)} _{𝑟𝑓} (R) (Y) = _{𝑟𝑓} (R) (Y) \underset{˙}{\cdot} _{𝑟𝑓} (R) (X)$
11	9 10	eqtrdi	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{\cdot} Y) = _{𝑟𝑓} (R) (Y) \underset{˙}{\cdot} _{𝑟𝑓} (R) (X)$
12		srngring	$⊢ R \in *-Ring \to R \in Ring$
13	2 3	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
14	12 13	syl3an1	$⊢ (R \in *-Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
15	2 1 5	stafval	$⊢ X \underset{˙}{\cdot} Y \in B \to _{𝑟𝑓} (R) (X \underset{˙}{\cdot} Y) = \underset{˙}{} (X \underset{˙}{\cdot} Y)$
16	14 15	syl	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{\cdot} Y) = \underset{˙}{*} (X \underset{˙}{\cdot} Y)$
17	2 1 5	stafval	$⊢ Y \in B \to _{𝑟𝑓} (R) (Y) = \underset{˙}{} (Y)$
18	17	3ad2ant3	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (Y) = \underset{˙}{*} (Y)$
19	2 1 5	stafval	$⊢ X \in B \to _{𝑟𝑓} (R) (X) = \underset{˙}{} (X)$
20	19	3ad2ant2	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X) = \underset{˙}{*} (X)$
21	18 20	oveq12d	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (Y) \underset{˙}{\cdot} _{𝑟𝑓} (R) (X) = \underset{˙}{} (Y) \underset{˙}{\cdot} \underset{˙}{*} (X)$
22	11 16 21	3eqtr3d	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to \underset{˙}{} (X \underset{˙}{\cdot} Y) = \underset{˙}{} (Y) \underset{˙}{\cdot} \underset{˙}{} (X)$

Metamath Proof Explorer

Theorem srngmul

Proof