This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldc

Description: The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020)

Ref Expression
Hypotheses drhmsubc.c ⊢ C = U ∩ DivRing
drhmsubc.j ⊢ J = r ∈ C , s ∈ C ⟼ r RingHom s
fldhmsubc.d ⊢ D = U ∩ Field
fldhmsubc.f ⊢ F = r ∈ D , s ∈ D ⟼ r RingHom s
Assertion fldc ⊢ U ∈ V → RingCat ⁡ U ↾ cat J ↾ cat F ∈ Cat

Proof

Step Hyp Ref Expression
1 drhmsubc.c ⊢ C = U ∩ DivRing
2 drhmsubc.j ⊢ J = r ∈ C , s ∈ C ⟼ r RingHom s
3 fldhmsubc.d ⊢ D = U ∩ Field
4 fldhmsubc.f ⊢ F = r ∈ D , s ∈ D ⟼ r RingHom s
5 fvexd ⊢ U ∈ V → RingCat ⁡ U ∈ V
6 ovex ⊢ r RingHom s ∈ V
7 2 6 fnmpoi ⊢ J Fn C × C
8 7 a1i ⊢ U ∈ V → J Fn C × C
9 4 6 fnmpoi ⊢ F Fn D × D
10 9 a1i ⊢ U ∈ V → F Fn D × D
11 inex1g ⊢ U ∈ V → U ∩ DivRing ∈ V
12 1 11 eqeltrid ⊢ U ∈ V → C ∈ V
13 df-field ⊢ Field = DivRing ∩ CRing
14 inss1 ⊢ DivRing ∩ CRing ⊆ DivRing
15 13 14 eqsstri ⊢ Field ⊆ DivRing
16 sslin ⊢ Field ⊆ DivRing → U ∩ Field ⊆ U ∩ DivRing
17 15 16 mp1i ⊢ U ∈ V → U ∩ Field ⊆ U ∩ DivRing
18 17 3 1 3sstr4g ⊢ U ∈ V → D ⊆ C
19 5 8 10 12 18 rescabs ⊢ U ∈ V → RingCat ⁡ U ↾ cat J ↾ cat F = RingCat ⁡ U ↾ cat F
20 1 2 3 4 fldcat ⊢ U ∈ V → RingCat ⁡ U ↾ cat F ∈ Cat
21 19 20 eqeltrd ⊢ U ∈ V → RingCat ⁡ U ↾ cat J ↾ cat F ∈ Cat