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