Theorem erngbase-rN

Description: The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom W ). (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.c-r	$$⊢C={\mathrm{Base}}_D$$
Assertion	erngbase-rN	$$⊢\left(K\in V\wedge W\in H\right)\to C=E$$

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.c-r	$$⊢C={\mathrm{Base}}_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 {\mathrm{Base}}_D={\mathrm{Base}}_{\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		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\}$$
10	9	rngbase	$$⊢E\in \mathrm{V}\to E={\mathrm{Base}}_{\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	8 10	ax-mp	$$⊢E={\mathrm{Base}}_{\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	7 5 11	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to C=E$$