Metamath Proof Explorer

Theorem fldhmsubc

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020)

Ref Expression
Hypotheses drhmsubc.c ⊢ 𝐶 = ( 𝑈 ∩ DivRing )
drhmsubc.j ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
fldhmsubc.d ⊢ 𝐷 = ( 𝑈 ∩ Field )
fldhmsubc.f ⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion fldhmsubc ( 𝑈 ∈ 𝑉 → 𝐹 ∈ ( Subcat ‘ ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 drhmsubc.c ⊢ 𝐶 = ( 𝑈 ∩ DivRing )
2 drhmsubc.j ⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3 fldhmsubc.d ⊢ 𝐷 = ( 𝑈 ∩ Field )
4 fldhmsubc.f ⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
5 elin ⊢ ( 𝑟 ∈ ( DivRing ∩ CRing ) ↔ ( 𝑟 ∈ DivRing ∧ 𝑟 ∈ CRing ) )
6 5 simprbi ⊢ ( 𝑟 ∈ ( DivRing ∩ CRing ) → 𝑟 ∈ CRing )
7 crngring ⊢ ( 𝑟 ∈ CRing → 𝑟 ∈ Ring )
8 6 7 syl ⊢ ( 𝑟 ∈ ( DivRing ∩ CRing ) → 𝑟 ∈ Ring )
9 df-field ⊢ Field = ( DivRing ∩ CRing )
10 8 9 eleq2s ⊢ ( 𝑟 ∈ Field → 𝑟 ∈ Ring )
11 10 rgen ⊢ ∀ 𝑟 ∈ Field 𝑟 ∈ Ring
12 11 3 4 srhmsubc ⊢ ( 𝑈 ∈ 𝑉 → 𝐹 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) )
13 inss1 ⊢ ( DivRing ∩ CRing ) ⊆ DivRing
14 9 13 eqsstri ⊢ Field ⊆ DivRing
15 sslin ⊢ ( Field ⊆ DivRing → ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
16 14 15 ax-mp ⊢ ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing )
17 16 a1i ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
18 3 1 sseq12i ⊢ ( 𝐷 ⊆ 𝐶 ↔ ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
19 17 18 sylibr ⊢ ( 𝑈 ∈ 𝑉 → 𝐷 ⊆ 𝐶 )
20 ssidd ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 RingHom 𝑦 ) ⊆ ( 𝑥 RingHom 𝑦 ) )
21 4 a1i ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) ) )
22 oveq12 ⊢ ( ( 𝑟 = 𝑥 ∧ 𝑠 = 𝑦 ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑥 RingHom 𝑦 ) )
23 22 adantl ⊢ ( ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ ( 𝑟 = 𝑥 ∧ 𝑠 = 𝑦 ) ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑥 RingHom 𝑦 ) )
24 simprl ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ∈ 𝐷 )
25 simpr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
26 25 adantl ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ∈ 𝐷 )
27 ovexd ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 RingHom 𝑦 ) ∈ V )
28 21 23 24 26 27 ovmpod ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
29 2 a1i ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) ) )
30 16 18 mpbir ⊢ 𝐷 ⊆ 𝐶
31 30 sseli ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ 𝐶 )
32 31 ad2antrl ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ∈ 𝐶 )
33 30 sseli ⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ 𝐶 )
34 33 adantl ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐶 )
35 34 adantl ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ∈ 𝐶 )
36 29 23 32 35 27 ovmpod ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 𝐽 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
37 20 28 36 3sstr4d ⊢ ( ( 𝑈 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 𝐹 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) )
38 37 ralrimivva ⊢ ( 𝑈 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 𝐹 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) )
39 ovex ⊢ ( 𝑟 RingHom 𝑠 ) ∈ V
40 4 39 fnmpoi ⊢ 𝐹 Fn ( 𝐷 × 𝐷 )
41 40 a1i ⊢ ( 𝑈 ∈ 𝑉 → 𝐹 Fn ( 𝐷 × 𝐷 ) )
42 2 39 fnmpoi ⊢ 𝐽 Fn ( 𝐶 × 𝐶 )
43 42 a1i ⊢ ( 𝑈 ∈ 𝑉 → 𝐽 Fn ( 𝐶 × 𝐶 ) )
44 inex1g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ DivRing ) ∈ V )
45 1 44 eqeltrid ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ V )
46 41 43 45 isssc ⊢ ( 𝑈 ∈ 𝑉 → ( 𝐹 ⊆cat 𝐽 ↔ ( 𝐷 ⊆ 𝐶 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 𝐹 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )
47 19 38 46 mpbir2and ⊢ ( 𝑈 ∈ 𝑉 → 𝐹 ⊆cat 𝐽 )
48 1 2 drhmsubc ⊢ ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) )
49 eqid ⊢ ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) = ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 )
50 49 subsubc ⊢ ( 𝐽 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) → ( 𝐹 ∈ ( Subcat ‘ ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ) ↔ ( 𝐹 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) ∧ 𝐹 ⊆cat 𝐽 ) ) )
51 48 50 syl ⊢ ( 𝑈 ∈ 𝑉 → ( 𝐹 ∈ ( Subcat ‘ ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ) ↔ ( 𝐹 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) ∧ 𝐹 ⊆cat 𝐽 ) ) )
52 12 47 51 mpbir2and ⊢ ( 𝑈 ∈ 𝑉 → 𝐹 ∈ ( Subcat ‘ ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ) )