Theorem erngplus

Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)

	Ref	Expression
Hypotheses	erngset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	erngset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	erngset.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	erngset.d	$$⊢D=\mathrm{EDRing}\left(K\right)\left(W\right)$$
	erng.p	$$⊢\underset{\dot{}}{+}={+}_D$$
Assertion	erngplus	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(U\in E\wedge V\in E\right)\right)\to U\underset{\dot{}}{+}V=\left(f\in T⟼U\left(f\right)\circ V\left(f\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		erngset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		erngset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		erngset.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		erngset.d	$$⊢D=\mathrm{EDRing}\left(K\right)\left(W\right)$$
5		erng.p	$$⊢\underset{\dot{}}{+}={+}_D$$
6	1 2 3 4 5	erngfplus	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)$$
7	6	oveqd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to U\underset{\dot{}}{+}V=U\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)V$$
8		eqid	$$⊢\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)=\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)$$
9	8 2	tendopl	$$⊢\left(U\in E\wedge V\in E\right)\to U\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)V=\left(f\in T⟼U\left(f\right)\circ V\left(f\right)\right)$$
10	7 9	sylan9eq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(U\in E\wedge V\in E\right)\right)\to U\underset{\dot{}}{+}V=\left(f\in T⟼U\left(f\right)\circ V\left(f\right)\right)$$