Theorem 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{\dot{}}{\ast }={\mathrm{*}}_R$$
	srngcl.b	$$⊢B={\mathrm{Base}}_R$$
	srngadd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	srngadd	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to \underset{\dot{}}{\ast }\left(X\underset{\dot{}}{+}Y\right)=\underset{\dot{}}{\ast }\left(X\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
2		srngcl.b	$$⊢B={\mathrm{Base}}_R$$
3		srngadd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
5		eqid	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
6	4 5	srngrhm	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{RingHom}{opp}_r\left(R\right)\right)$$
7		rhmghm	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{RingHom}{opp}_r\left(R\right)\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{GrpHom}{opp}_r\left(R\right)\right)$$
8	6 7	syl	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{GrpHom}{opp}_r\left(R\right)\right)$$
9	4 3	oppradd	$$⊢\underset{\dot{}}{+}={+}_{{opp}_r\left(R\right)}$$
10	2 3 9	ghmlin	$$⊢\left({\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{GrpHom}{opp}_r\left(R\right)\right)\wedge X\in B\wedge Y\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\underset{\dot{}}{+}Y\right)={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)\underset{\dot{}}{+}{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(Y\right)$$
11	8 10	syl3an1	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\underset{\dot{}}{+}Y\right)={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)\underset{\dot{}}{+}{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(Y\right)$$
12		srngring	$$⊢R\in \mathrm{*-Ring}\to R\in \mathrm{Ring}$$
13	2 3	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
14	12 13	syl3an1	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
15	2 1 5	stafval	$$⊢X\underset{\dot{}}{+}Y\in B\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\underset{\dot{}}{+}Y\right)=\underset{\dot{}}{\ast }\left(X\underset{\dot{}}{+}Y\right)$$
16	14 15	syl	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\underset{\dot{}}{+}Y\right)=\underset{\dot{}}{\ast }\left(X\underset{\dot{}}{+}Y\right)$$
17	2 1 5	stafval	$$⊢X\in B\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)=\underset{\dot{}}{\ast }\left(X\right)$$
18	17	3ad2ant2	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)=\underset{\dot{}}{\ast }\left(X\right)$$
19	2 1 5	stafval	$$⊢Y\in B\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(Y\right)=\underset{\dot{}}{\ast }\left(Y\right)$$
20	19	3ad2ant3	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(Y\right)=\underset{\dot{}}{\ast }\left(Y\right)$$
21	18 20	oveq12d	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)\underset{\dot{}}{+}{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(Y\right)=\underset{\dot{}}{\ast }\left(X\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(Y\right)$$
22	11 16 21	3eqtr3d	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\wedge Y\in B\right)\to \underset{\dot{}}{\ast }\left(X\underset{\dot{}}{+}Y\right)=\underset{\dot{}}{\ast }\left(X\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(Y\right)$$