srngadd

Description: The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	srngcl.i	$⊢ \underset{˙}{} = _{R}$
	srngcl.b	$⊢ B = {Base}_{R}$
	srngadd.p	$⊢ \underset{˙}{+} = +_{R}$
Assertion	srngadd	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to \underset{˙}{} (X \underset{˙}{+} Y) = \underset{˙}{} (X) \underset{˙}{+} \underset{˙}{} (Y)$

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	$⊢ \underset{˙}{} = _{R}$
2		srngcl.b	$⊢ B = {Base}_{R}$
3		srngadd.p	$⊢ \underset{˙}{+} = +_{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		rhmghm	$⊢ _{𝑟𝑓} (R) \in (R RingHom {opp}_{r} (R)) \to _{𝑟𝑓} (R) \in (R GrpHom {opp}_{r} (R))$
8	6 7	syl	$⊢ R \in -Ring \to _{𝑟𝑓} (R) \in (R GrpHom {opp}_{r} (R))$
9	4 3	oppradd	$⊢ \underset{˙}{+} = +_{{opp}_{r} (R)}$
10	2 3 9	ghmlin	$⊢ (_{𝑟𝑓} (R) \in (R GrpHom {opp}_{r} (R)) \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{+} Y) = _{𝑟𝑓} (R) (X) \underset{˙}{+} _{𝑟𝑓} (R) (Y)$
11	8 10	syl3an1	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{+} Y) = _{𝑟𝑓} (R) (X) \underset{˙}{+} _{𝑟𝑓} (R) (Y)$
12		srngring	$⊢ R \in *-Ring \to R \in Ring$
13	2 3	ringacl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
14	12 13	syl3an1	$⊢ (R \in *-Ring \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
15	2 1 5	stafval	$⊢ X \underset{˙}{+} Y \in B \to _{𝑟𝑓} (R) (X \underset{˙}{+} Y) = \underset{˙}{} (X \underset{˙}{+} Y)$
16	14 15	syl	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X \underset{˙}{+} Y) = \underset{˙}{*} (X \underset{˙}{+} Y)$
17	2 1 5	stafval	$⊢ X \in B \to _{𝑟𝑓} (R) (X) = \underset{˙}{} (X)$
18	17	3ad2ant2	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X) = \underset{˙}{*} (X)$
19	2 1 5	stafval	$⊢ Y \in B \to _{𝑟𝑓} (R) (Y) = \underset{˙}{} (Y)$
20	19	3ad2ant3	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (Y) = \underset{˙}{*} (Y)$
21	18 20	oveq12d	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to _{𝑟𝑓} (R) (X) \underset{˙}{+} _{𝑟𝑓} (R) (Y) = \underset{˙}{} (X) \underset{˙}{+} \underset{˙}{*} (Y)$
22	11 16 21	3eqtr3d	$⊢ (R \in -Ring \land X \in B \land Y \in B) \to \underset{˙}{} (X \underset{˙}{+} Y) = \underset{˙}{} (X) \underset{˙}{+} \underset{˙}{} (Y)$

Metamath Proof Explorer

Theorem srngadd

Proof