Metamath Proof Explorer


Theorem fldcALTV

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) (New usage is discouraged.)

Ref Expression
Hypotheses drhmsubcALTV.c 𝐶 = ( 𝑈 ∩ DivRing )
drhmsubcALTV.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
fldhmsubcALTV.d 𝐷 = ( 𝑈 ∩ Field )
fldhmsubcALTV.f 𝐹 = ( 𝑟𝐷 , 𝑠𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion fldcALTV ( 𝑈𝑉 → ( ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) ∈ Cat )

Proof

Step Hyp Ref Expression
1 drhmsubcALTV.c 𝐶 = ( 𝑈 ∩ DivRing )
2 drhmsubcALTV.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3 fldhmsubcALTV.d 𝐷 = ( 𝑈 ∩ Field )
4 fldhmsubcALTV.f 𝐹 = ( 𝑟𝐷 , 𝑠𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
5 fvexd ( 𝑈𝑉 → ( RingCatALTV ‘ 𝑈 ) ∈ 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 ( 𝑈𝑉 → ( ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) = ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐹 ) )
20 1 2 3 4 fldcatALTV ( 𝑈𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐹 ) ∈ Cat )
21 19 20 eqeltrd ( 𝑈𝑉 → ( ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) ∈ Cat )