Theorem erngbase

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 ). TODO: the .t hypothesis isn't used. (Also look at others.) (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.c	$$⊢C={\mathrm{Base}}_D$$
Assertion	erngbase	$$⊢\left(K\in V\wedge W\in H\right)\to C=E$$

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.c	$$⊢C={\mathrm{Base}}_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 {\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⟼s\circ t\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⟼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\}$$
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⟼s\circ t\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⟼s\circ t\right)⟩\right\}}$$
12	7 5 11	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to C=E$$