Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nsgqusf1o Structured version   Visualization version   GIF version

Theorem nsgqusf1o 32572
Description: The canonical projection homomorphism 𝐸 defines a bijective correspondence between the set 𝑆 of subgroups of 𝐺 containing a normal subgroup 𝑁 and the subgroups of the quotient group 𝐺 / 𝑁. This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024.)
Hypotheses
Ref Expression
nsgqusf1o.b 𝐡 = (Baseβ€˜πΊ)
nsgqusf1o.s 𝑆 = {β„Ž ∈ (SubGrpβ€˜πΊ) ∣ 𝑁 βŠ† β„Ž}
nsgqusf1o.t 𝑇 = (SubGrpβ€˜π‘„)
nsgqusf1o.1 ≀ = (leβ€˜(toIncβ€˜π‘†))
nsgqusf1o.2 ≲ = (leβ€˜(toIncβ€˜π‘‡))
nsgqusf1o.q 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))
nsgqusf1o.p βŠ• = (LSSumβ€˜πΊ)
nsgqusf1o.e 𝐸 = (β„Ž ∈ 𝑆 ↦ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)))
nsgqusf1o.f 𝐹 = (𝑓 ∈ 𝑇 ↦ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
nsgqusf1o.n (πœ‘ β†’ 𝑁 ∈ (NrmSGrpβ€˜πΊ))
Assertion
Ref Expression
nsgqusf1o (πœ‘ β†’ 𝐸:𝑆–1-1-onto→𝑇)
Distinct variable groups:   βŠ• ,π‘Ž,𝑓,β„Ž,π‘₯   𝐡,π‘Ž,𝑓,β„Ž,π‘₯   𝐸,π‘Ž,𝑓,β„Ž,π‘₯   𝑓,𝐹,β„Ž,π‘₯   𝐺,π‘Ž,𝑓,β„Ž,π‘₯   𝑁,π‘Ž,𝑓,β„Ž,π‘₯   𝑄,π‘Ž,𝑓,β„Ž,π‘₯   𝑆,π‘Ž,𝑓,β„Ž,π‘₯   𝑇,π‘Ž,𝑓,β„Ž,π‘₯   πœ‘,π‘Ž,𝑓,β„Ž,π‘₯
Allowed substitution hints:   𝐹(π‘Ž)   ≀ (π‘₯,𝑓,β„Ž,π‘Ž)   ≲ (π‘₯,𝑓,β„Ž,π‘Ž)

Proof of Theorem nsgqusf1o
StepHypRef Expression
1 eqid 2732 . . . 4 ((toIncβ€˜π‘†)MGalConn(toIncβ€˜π‘‡)) = ((toIncβ€˜π‘†)MGalConn(toIncβ€˜π‘‡))
2 nsgqusf1o.s . . . . . 6 𝑆 = {β„Ž ∈ (SubGrpβ€˜πΊ) ∣ 𝑁 βŠ† β„Ž}
3 fvex 6904 . . . . . 6 (SubGrpβ€˜πΊ) ∈ V
42, 3rabex2 5334 . . . . 5 𝑆 ∈ V
5 eqid 2732 . . . . . 6 (toIncβ€˜π‘†) = (toIncβ€˜π‘†)
65ipobas 18486 . . . . 5 (𝑆 ∈ V β†’ 𝑆 = (Baseβ€˜(toIncβ€˜π‘†)))
74, 6ax-mp 5 . . . 4 𝑆 = (Baseβ€˜(toIncβ€˜π‘†))
8 nsgqusf1o.t . . . . . 6 𝑇 = (SubGrpβ€˜π‘„)
98fvexi 6905 . . . . 5 𝑇 ∈ V
10 eqid 2732 . . . . . 6 (toIncβ€˜π‘‡) = (toIncβ€˜π‘‡)
1110ipobas 18486 . . . . 5 (𝑇 ∈ V β†’ 𝑇 = (Baseβ€˜(toIncβ€˜π‘‡)))
129, 11ax-mp 5 . . . 4 𝑇 = (Baseβ€˜(toIncβ€˜π‘‡))
13 nsgqusf1o.1 . . . 4 ≀ = (leβ€˜(toIncβ€˜π‘†))
14 nsgqusf1o.2 . . . 4 ≲ = (leβ€˜(toIncβ€˜π‘‡))
155ipopos 18491 . . . . 5 (toIncβ€˜π‘†) ∈ Poset
1615a1i 11 . . . 4 (πœ‘ β†’ (toIncβ€˜π‘†) ∈ Poset)
1710ipopos 18491 . . . . 5 (toIncβ€˜π‘‡) ∈ Poset
1817a1i 11 . . . 4 (πœ‘ β†’ (toIncβ€˜π‘‡) ∈ Poset)
19 nsgqusf1o.b . . . . 5 𝐡 = (Baseβ€˜πΊ)
20 nsgqusf1o.q . . . . 5 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))
21 nsgqusf1o.p . . . . 5 βŠ• = (LSSumβ€˜πΊ)
22 nsgqusf1o.e . . . . 5 𝐸 = (β„Ž ∈ 𝑆 ↦ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)))
23 nsgqusf1o.f . . . . 5 𝐹 = (𝑓 ∈ 𝑇 ↦ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
24 nsgqusf1o.n . . . . 5 (πœ‘ β†’ 𝑁 ∈ (NrmSGrpβ€˜πΊ))
2519, 2, 8, 1, 5, 10, 20, 21, 22, 23, 24nsgmgc 32568 . . . 4 (πœ‘ β†’ 𝐸((toIncβ€˜π‘†)MGalConn(toIncβ€˜π‘‡))𝐹)
261, 7, 12, 13, 14, 16, 18, 25mgcf1o 32211 . . 3 (πœ‘ β†’ (𝐸 β†Ύ ran 𝐹) Isom ≀ , ≲ (ran 𝐹, ran 𝐸))
27 isof1o 7322 . . 3 ((𝐸 β†Ύ ran 𝐹) Isom ≀ , ≲ (ran 𝐹, ran 𝐸) β†’ (𝐸 β†Ύ ran 𝐹):ran 𝐹–1-1-ontoβ†’ran 𝐸)
2826, 27syl 17 . 2 (πœ‘ β†’ (𝐸 β†Ύ ran 𝐹):ran 𝐹–1-1-ontoβ†’ran 𝐸)
2919, 2, 8, 13, 14, 20, 21, 22, 23, 24nsgqusf1olem3 32571 . . . . 5 (πœ‘ β†’ ran 𝐹 = 𝑆)
3029reseq2d 5981 . . . 4 (πœ‘ β†’ (𝐸 β†Ύ ran 𝐹) = (𝐸 β†Ύ 𝑆))
31 nfv 1917 . . . . . 6 β„²β„Žπœ‘
32 vex 3478 . . . . . . . . 9 β„Ž ∈ V
3332mptex 7227 . . . . . . . 8 (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) ∈ V
3433rnex 7905 . . . . . . 7 ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) ∈ V
3534a1i 11 . . . . . 6 ((πœ‘ ∧ β„Ž ∈ 𝑆) β†’ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) ∈ V)
3631, 35, 22fnmptd 6691 . . . . 5 (πœ‘ β†’ 𝐸 Fn 𝑆)
37 fnresdm 6669 . . . . 5 (𝐸 Fn 𝑆 β†’ (𝐸 β†Ύ 𝑆) = 𝐸)
3836, 37syl 17 . . . 4 (πœ‘ β†’ (𝐸 β†Ύ 𝑆) = 𝐸)
3930, 38eqtrd 2772 . . 3 (πœ‘ β†’ (𝐸 β†Ύ ran 𝐹) = 𝐸)
4019, 2, 8, 13, 14, 20, 21, 22, 23, 24nsgqusf1olem2 32570 . . 3 (πœ‘ β†’ ran 𝐸 = 𝑇)
4139, 29, 40f1oeq123d 6827 . 2 (πœ‘ β†’ ((𝐸 β†Ύ ran 𝐹):ran 𝐹–1-1-ontoβ†’ran 𝐸 ↔ 𝐸:𝑆–1-1-onto→𝑇))
4228, 41mpbid 231 1 (πœ‘ β†’ 𝐸:𝑆–1-1-onto→𝑇)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3432  Vcvv 3474   βŠ† wss 3948  {csn 4628   ↦ cmpt 5231  ran crn 5677   β†Ύ cres 5678   Fn wfn 6538  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7411  Basecbs 17146  lecple 17206   /s cqus 17453  Posetcpo 18262  toInccipo 18482  SubGrpcsubg 19002  NrmSGrpcnsg 19003   ~QG cqg 19004  LSSumclsm 19504  MGalConncmgc 32187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-fz 13487  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ocomp 17220  df-ds 17221  df-0g 17389  df-imas 17456  df-qus 17457  df-proset 18250  df-poset 18268  df-ipo 18483  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-submnd 18674  df-grp 18824  df-minusg 18825  df-subg 19005  df-nsg 19006  df-eqg 19007  df-ghm 19092  df-oppg 19212  df-lsm 19506  df-mnt 32188  df-mgc 32189
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator