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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	erngset.t-r	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	erngset.e-r	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	erngset.d-r	⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
	erng.c-r	⊢ 𝐶 = ( Base ‘ 𝐷 )
Assertion	erngbase-rN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		erngset.h-r	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		erngset.t-r	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		erngset.e-r	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4		erngset.d-r	⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
5		erng.c-r	⊢ 𝐶 = ( Base ‘ 𝐷 )
6	1 2 3 4	erngset-rN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } )
7	6	fveq2d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } ) )
8	3	fvexi	⊢ 𝐸 ∈ V
9		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ }
10	9	rngbase	⊢ ( 𝐸 ∈ V → 𝐸 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } ) )
11	8 10	ax-mp	⊢ 𝐸 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } )
12	7 5 11	3eqtr4g	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐶 = 𝐸 )