Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fldhmsubc Structured version   Visualization version   GIF version

Theorem fldhmsubc 41393
Description: According to df-subc 16400, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 ( see subcssc 16428 and subcss2 16431). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.)
Hypotheses
Ref Expression
drhmsubc.c 𝐶 = (𝑈 ∩ DivRing)
drhmsubc.j 𝐽 = (𝑟𝐶, 𝑠𝐶 ↦ (𝑟 RingHom 𝑠))
fldhmsubc.d 𝐷 = (𝑈 ∩ Field)
fldhmsubc.f 𝐹 = (𝑟𝐷, 𝑠𝐷 ↦ (𝑟 RingHom 𝑠))
Assertion
Ref Expression
fldhmsubc (𝑈𝑉𝐹 ∈ (Subcat‘((RingCat‘𝑈) ↾cat 𝐽)))
Distinct variable groups:   𝐶,𝑟,𝑠   𝑈,𝑟,𝑠   𝑉,𝑟,𝑠   𝐷,𝑟,𝑠
Allowed substitution hints:   𝐹(𝑠,𝑟)   𝐽(𝑠,𝑟)

Proof of Theorem fldhmsubc
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elin 3779 . . . . . . 7 (𝑟 ∈ (DivRing ∩ CRing) ↔ (𝑟 ∈ DivRing ∧ 𝑟 ∈ CRing))
21simprbi 480 . . . . . 6 (𝑟 ∈ (DivRing ∩ CRing) → 𝑟 ∈ CRing)
3 crngring 18486 . . . . . 6 (𝑟 ∈ CRing → 𝑟 ∈ Ring)
42, 3syl 17 . . . . 5 (𝑟 ∈ (DivRing ∩ CRing) → 𝑟 ∈ Ring)
5 df-field 18678 . . . . 5 Field = (DivRing ∩ CRing)
64, 5eleq2s 2716 . . . 4 (𝑟 ∈ Field → 𝑟 ∈ Ring)
76rgen 2917 . . 3 𝑟 ∈ Field 𝑟 ∈ Ring
8 fldhmsubc.d . . 3 𝐷 = (𝑈 ∩ Field)
9 fldhmsubc.f . . 3 𝐹 = (𝑟𝐷, 𝑠𝐷 ↦ (𝑟 RingHom 𝑠))
107, 8, 9srhmsubc 41385 . 2 (𝑈𝑉𝐹 ∈ (Subcat‘(RingCat‘𝑈)))
11 inss1 3816 . . . . . . 7 (DivRing ∩ CRing) ⊆ DivRing
125, 11eqsstri 3619 . . . . . 6 Field ⊆ DivRing
13 sslin 3822 . . . . . 6 (Field ⊆ DivRing → (𝑈 ∩ Field) ⊆ (𝑈 ∩ DivRing))
1412, 13ax-mp 5 . . . . 5 (𝑈 ∩ Field) ⊆ (𝑈 ∩ DivRing)
1514a1i 11 . . . 4 (𝑈𝑉 → (𝑈 ∩ Field) ⊆ (𝑈 ∩ DivRing))
16 drhmsubc.c . . . . 5 𝐶 = (𝑈 ∩ DivRing)
178, 16sseq12i 3615 . . . 4 (𝐷𝐶 ↔ (𝑈 ∩ Field) ⊆ (𝑈 ∩ DivRing))
1815, 17sylibr 224 . . 3 (𝑈𝑉𝐷𝐶)
19 ssid 3608 . . . . . 6 (𝑥 RingHom 𝑦) ⊆ (𝑥 RingHom 𝑦)
2019a1i 11 . . . . 5 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → (𝑥 RingHom 𝑦) ⊆ (𝑥 RingHom 𝑦))
219a1i 11 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → 𝐹 = (𝑟𝐷, 𝑠𝐷 ↦ (𝑟 RingHom 𝑠)))
22 oveq12 6619 . . . . . . 7 ((𝑟 = 𝑥𝑠 = 𝑦) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦))
2322adantl 482 . . . . . 6 (((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) ∧ (𝑟 = 𝑥𝑠 = 𝑦)) → (𝑟 RingHom 𝑠) = (𝑥 RingHom 𝑦))
24 simprl 793 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → 𝑥𝐷)
25 simpr 477 . . . . . . 7 ((𝑥𝐷𝑦𝐷) → 𝑦𝐷)
2625adantl 482 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → 𝑦𝐷)
27 ovex 6638 . . . . . . 7 (𝑥 RingHom 𝑦) ∈ V
2827a1i 11 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → (𝑥 RingHom 𝑦) ∈ V)
2921, 23, 24, 26, 28ovmpt2d 6748 . . . . 5 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → (𝑥𝐹𝑦) = (𝑥 RingHom 𝑦))
30 drhmsubc.j . . . . . . 7 𝐽 = (𝑟𝐶, 𝑠𝐶 ↦ (𝑟 RingHom 𝑠))
3130a1i 11 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → 𝐽 = (𝑟𝐶, 𝑠𝐶 ↦ (𝑟 RingHom 𝑠)))
3214, 17mpbir 221 . . . . . . . 8 𝐷𝐶
3332sseli 3583 . . . . . . 7 (𝑥𝐷𝑥𝐶)
3433ad2antrl 763 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → 𝑥𝐶)
3532sseli 3583 . . . . . . . 8 (𝑦𝐷𝑦𝐶)
3635adantl 482 . . . . . . 7 ((𝑥𝐷𝑦𝐷) → 𝑦𝐶)
3736adantl 482 . . . . . 6 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → 𝑦𝐶)
3831, 23, 34, 37, 28ovmpt2d 6748 . . . . 5 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → (𝑥𝐽𝑦) = (𝑥 RingHom 𝑦))
3920, 29, 383sstr4d 3632 . . . 4 ((𝑈𝑉 ∧ (𝑥𝐷𝑦𝐷)) → (𝑥𝐹𝑦) ⊆ (𝑥𝐽𝑦))
4039ralrimivva 2966 . . 3 (𝑈𝑉 → ∀𝑥𝐷𝑦𝐷 (𝑥𝐹𝑦) ⊆ (𝑥𝐽𝑦))
41 ovex 6638 . . . . . 6 (𝑟 RingHom 𝑠) ∈ V
429, 41fnmpt2i 7191 . . . . 5 𝐹 Fn (𝐷 × 𝐷)
4342a1i 11 . . . 4 (𝑈𝑉𝐹 Fn (𝐷 × 𝐷))
4430, 41fnmpt2i 7191 . . . . 5 𝐽 Fn (𝐶 × 𝐶)
4544a1i 11 . . . 4 (𝑈𝑉𝐽 Fn (𝐶 × 𝐶))
46 inex1g 4766 . . . . 5 (𝑈𝑉 → (𝑈 ∩ DivRing) ∈ V)
4716, 46syl5eqel 2702 . . . 4 (𝑈𝑉𝐶 ∈ V)
4843, 45, 47isssc 16408 . . 3 (𝑈𝑉 → (𝐹cat 𝐽 ↔ (𝐷𝐶 ∧ ∀𝑥𝐷𝑦𝐷 (𝑥𝐹𝑦) ⊆ (𝑥𝐽𝑦))))
4918, 40, 48mpbir2and 956 . 2 (𝑈𝑉𝐹cat 𝐽)
5016, 30drhmsubc 41389 . . 3 (𝑈𝑉𝐽 ∈ (Subcat‘(RingCat‘𝑈)))
51 eqid 2621 . . . 4 ((RingCat‘𝑈) ↾cat 𝐽) = ((RingCat‘𝑈) ↾cat 𝐽)
5251subsubc 16441 . . 3 (𝐽 ∈ (Subcat‘(RingCat‘𝑈)) → (𝐹 ∈ (Subcat‘((RingCat‘𝑈) ↾cat 𝐽)) ↔ (𝐹 ∈ (Subcat‘(RingCat‘𝑈)) ∧ 𝐹cat 𝐽)))
5350, 52syl 17 . 2 (𝑈𝑉 → (𝐹 ∈ (Subcat‘((RingCat‘𝑈) ↾cat 𝐽)) ↔ (𝐹 ∈ (Subcat‘(RingCat‘𝑈)) ∧ 𝐹cat 𝐽)))
5410, 49, 53mpbir2and 956 1 (𝑈𝑉𝐹 ∈ (Subcat‘((RingCat‘𝑈) ↾cat 𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  Vcvv 3189  cin 3558  wss 3559   class class class wbr 4618   × cxp 5077   Fn wfn 5847  cfv 5852  (class class class)co 6610  cmpt2 6612  cat cssc 16395  cat cresc 16396  Subcatcsubc 16397  Ringcrg 18475  CRingccrg 18476   RingHom crh 18640  DivRingcdr 18675  Fieldcfield 18676  RingCatcringc 41312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-fz 12276  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-hom 15894  df-cco 15895  df-0g 16030  df-cat 16257  df-cid 16258  df-homf 16259  df-ssc 16398  df-resc 16399  df-subc 16400  df-estrc 16691  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-mhm 17263  df-grp 17353  df-ghm 17586  df-mgp 18418  df-ur 18430  df-ring 18477  df-cring 18478  df-rnghom 18643  df-drng 18677  df-field 18678  df-ringc 41314
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator