Theorem erngfmul-rN

Description: Ring multiplication operation. (Contributed by NM, 9-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	erngset.h-r	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	erngset.t-r	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	erngset.e-r	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	erngset.d-r	$$⊢D={\mathrm{EDRing}}_R\left(K\right)\left(W\right)$$
	erng.m-r	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
Assertion	erngfmul-rN	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\left(s\in E,t\in E⟼t\circ s\right)$$

Proof

Step	Hyp	Ref	Expression
1		erngset.h-r	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		erngset.t-r	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		erngset.e-r	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		erngset.d-r	$$⊢D={\mathrm{EDRing}}_R\left(K\right)\left(W\right)$$
5		erng.m-r	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
6	1 2 3 4	erngset-rN	$$⊢\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⟼t\circ s\right)⟩\right\}$$
7	6	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {\cdot }_D={\cdot }_{\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⟼t\circ s\right)⟩\right\}}$$
8	3	fvexi	$$⊢E\in \mathrm{V}$$
9	8 8	mpoex	$$⊢\left(s\in E,t\in E⟼t\circ s\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⟼t\circ s\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⟼t\circ s\right)⟩\right\}$$
11	10	rngmulr	$$⊢\left(s\in E,t\in E⟼t\circ s\right)\in \mathrm{V}\to \left(s\in E,t\in E⟼t\circ s\right)={\cdot }_{\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⟼t\circ s\right)⟩\right\}}$$
12	9 11	ax-mp	$$⊢\left(s\in E,t\in E⟼t\circ s\right)={\cdot }_{\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⟼t\circ s\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⟼t\circ s\right)$$