erngset-rN

Description: The division ring on trace-preserving endomorphisms for a fiducial co-atom W . (Contributed by NM, 5-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	erngset.h-r	$⊢ H = LHyp (K)$
	erngset.t-r	$⊢ T = LTrn (K) (W)$
	erngset.e-r	$⊢ E = TEndo (K) (W)$
	erngset.d-r	$⊢ D = {EDRing}_{R} (K) (W)$
Assertion	erngset-rN	$⊢ (K \in V \land W \in H) \to D = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩\}$

Proof

Step	Hyp	Ref	Expression
1		erngset.h-r	$⊢ H = LHyp (K)$
2		erngset.t-r	$⊢ T = LTrn (K) (W)$
3		erngset.e-r	$⊢ E = TEndo (K) (W)$
4		erngset.d-r	$⊢ D = {EDRing}_{R} (K) (W)$
5	1	erngfset-rN	$⊢ K \in V \to {EDRing}_{R} (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\})$
6	5	fveq1d	$⊢ K \in V \to {EDRing}_{R} (K) (W) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}) (W)$
7	4 6	syl5eq	$⊢ K \in V \to D = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}) (W)$
8		fveq2	$⊢ w = W \to TEndo (K) (w) = TEndo (K) (W)$
9	8	opeq2d	$⊢ w = W \to ⟨{Base}_{ndx}, TEndo (K) (w)⟩ = ⟨{Base}_{ndx}, TEndo (K) (W)⟩$
10		tpeq1	$⊢ ⟨{Base}_{ndx}, TEndo (K) (w)⟩ = ⟨{Base}_{ndx}, TEndo (K) (W)⟩ \to \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, TEndo (K) (W)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}$
11	3	opeq2i	$⊢ ⟨{Base}_{ndx}, E⟩ = ⟨{Base}_{ndx}, TEndo (K) (W)⟩$
12		tpeq1	$⊢ ⟨{Base}_{ndx}, E⟩ = ⟨{Base}_{ndx}, TEndo (K) (W)⟩ \to \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, TEndo (K) (W)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}$
13	11 12	ax-mp	$⊢ \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, TEndo (K) (W)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}$
14	10 13	eqtr4di	$⊢ ⟨{Base}_{ndx}, TEndo (K) (w)⟩ = ⟨{Base}_{ndx}, TEndo (K) (W)⟩ \to \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}$
15	9 14	syl	$⊢ w = W \to \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}$
16	8 3	eqtr4di	$⊢ w = W \to TEndo (K) (w) = E$
17		fveq2	$⊢ w = W \to LTrn (K) (w) = LTrn (K) (W)$
18	17 2	eqtr4di	$⊢ w = W \to LTrn (K) (w) = T$
19		eqidd	$⊢ w = W \to s (f) \circ t (f) = s (f) \circ t (f)$
20	18 19	mpteq12dv	$⊢ w = W \to (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)) = (f \in T ⟼ s (f) \circ t (f))$
21	16 16 20	mpoeq123dv	$⊢ w = W \to (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f))) = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
22	21	opeq2d	$⊢ w = W \to ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩ = ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩$
23	22	tpeq2d	$⊢ w = W \to \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}$
24		eqidd	$⊢ w = W \to t \circ s = t \circ s$
25	16 16 24	mpoeq123dv	$⊢ w = W \to (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s) = (s \in E, t \in E ⟼ t \circ s)$
26	25	opeq2d	$⊢ w = W \to ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩ = ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩$
27	26	tpeq3d	$⊢ w = W \to \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩\}$
28	15 23 27	3eqtrd	$⊢ w = W \to \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\} = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩\}$
29		eqid	$⊢ (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\})$
30		tpex	$⊢ \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩\} \in V$
31	28 29 30	fvmpt	$⊢ W \in H \to (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩\}) (W) = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩\}$
32	7 31	sylan9eq	$⊢ (K \in V \land W \in H) \to D = \{⟨{Base}_{ndx}, E⟩, ⟨+_{ndx}, (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in E, t \in E ⟼ t \circ s)⟩\}$

Metamath Proof Explorer

Theorem erngset-rN

Proof