Theorem erngfplus

Description: Ring addition operation. (Contributed by NM, 9-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	erngfplus	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\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	erngset	$$⊢\left(K\in V\wedge W\in H\right)\to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},E⟩,⟨{+}_{\mathrm{ndx}},\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in E,t\in E⟼s\circ t\right)⟩\right\}$$
7	6	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {+}_D={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},E⟩,⟨{+}_{\mathrm{ndx}},\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in E,t\in E⟼s\circ t\right)⟩\right\}}$$
8	3	fvexi	$$⊢E\in \mathrm{V}$$
9	8 8	mpoex	$$⊢\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)\in \mathrm{V}$$
10		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},E⟩,⟨{+}_{\mathrm{ndx}},\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in E,t\in E⟼s\circ t\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},E⟩,⟨{+}_{\mathrm{ndx}},\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in E,t\in E⟼s\circ t\right)⟩\right\}$$
11	10	rngplusg	$$⊢\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)\in \mathrm{V}\to \left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},E⟩,⟨{+}_{\mathrm{ndx}},\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in E,t\in E⟼s\circ t\right)⟩\right\}}$$
12	9 11	ax-mp	$$⊢\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},E⟩,⟨{+}_{\mathrm{ndx}},\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in E,t\in E⟼s\circ t\right)⟩\right\}}$$
13	7 5 12	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$