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 ⊢ 𝐶 = ( 𝑈 ∩ DivRing )
drhmsubc.j ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
fldhmsubc.d ⊢ 𝐷 = ( 𝑈 ∩ Field )
fldhmsubc.f ⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion fldc ( 𝑈 ∈ 𝑉 → ( ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) ∈ Cat )

Proof

Step Hyp Ref Expression
1 drhmsubc.c ⊢ 𝐶 = ( 𝑈 ∩ DivRing )
2 drhmsubc.j ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3 fldhmsubc.d ⊢ 𝐷 = ( 𝑈 ∩ Field )
4 fldhmsubc.f ⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
5 fvexd ⊢ ( 𝑈 ∈ 𝑉 → ( RingCat ‘ 𝑈 ) ∈ V )
6 ovex ⊢ ( 𝑟 RingHom 𝑠 ) ∈ V
7 2 6 fnmpoi ⊢ 𝐽 Fn ( 𝐶 × 𝐶 )
8 7 a1i ⊢ ( 𝑈 ∈ 𝑉 → 𝐽 Fn ( 𝐶 × 𝐶 ) )
9 4 6 fnmpoi ⊢ 𝐹 Fn ( 𝐷 × 𝐷 )
10 9 a1i ⊢ ( 𝑈 ∈ 𝑉 → 𝐹 Fn ( 𝐷 × 𝐷 ) )
11 inex1g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ DivRing ) ∈ V )
12 1 11 eqeltrid ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ V )
13 df-field ⊢ Field = ( DivRing ∩ CRing )
14 inss1 ⊢ ( DivRing ∩ CRing ) ⊆ DivRing
15 13 14 eqsstri ⊢ Field ⊆ DivRing
16 sslin ⊢ ( Field ⊆ DivRing → ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
17 15 16 mp1i ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
18 17 3 1 3sstr4g ⊢ ( 𝑈 ∈ 𝑉 → 𝐷 ⊆ 𝐶 )
19 5 8 10 12 18 rescabs ⊢ ( 𝑈 ∈ 𝑉 → ( ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) = ( ( RingCat ‘ 𝑈 ) ↾cat 𝐹 ) )
20 1 2 3 4 fldcat ⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾cat 𝐹 ) ∈ Cat )
21 19 20 eqeltrd ⊢ ( 𝑈 ∈ 𝑉 → ( ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) ∈ Cat )