Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ghomdiv Structured version   Visualization version   GIF version
Theorem ghomdiv 36755
Description: Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
Hypotheses
Ref Expression
ghomdiv.1 𝑋 = ran 𝐺
ghomdiv.2 𝐷 = ( /𝑔 β€˜πΊ)
ghomdiv.3 𝐢 = ( /𝑔 β€˜π»)
Assertion
Ref Expression
ghomdiv (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜(𝐴𝐷𝐡)) = ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅)))
Proof of Theorem ghomdiv
StepHypRef Expression
1 simpl2 1192 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ 𝐻 ∈ GrpOp)
2 ghomdiv.1 . . . . . . 7 𝑋 = ran 𝐺
3 eqid 2732 . . . . . . 7 ran 𝐻 = ran 𝐻
42, 3ghomf 36753 . . . . . 6 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) β†’ 𝐹:π‘‹βŸΆran 𝐻)
54ffvelcdmda 7086 . . . . 5 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ 𝐴 ∈ 𝑋) β†’ (πΉβ€˜π΄) ∈ ran 𝐻)
65adantrr 715 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜π΄) ∈ ran 𝐻)
74ffvelcdmda 7086 . . . . 5 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ 𝐡 ∈ 𝑋) β†’ (πΉβ€˜π΅) ∈ ran 𝐻)
87adantrl 714 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜π΅) ∈ ran 𝐻)
9 ghomdiv.3 . . . . 5 𝐢 = ( /𝑔 β€˜π»)
103, 9grponpcan 29791 . . . 4 ((𝐻 ∈ GrpOp ∧ (πΉβ€˜π΄) ∈ ran 𝐻 ∧ (πΉβ€˜π΅) ∈ ran 𝐻) β†’ (((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))𝐻(πΉβ€˜π΅)) = (πΉβ€˜π΄))
111, 6, 8, 10syl3anc 1371 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))𝐻(πΉβ€˜π΅)) = (πΉβ€˜π΄))
12 ghomdiv.2 . . . . . . 7 𝐷 = ( /𝑔 β€˜πΊ)
132, 12grponpcan 29791 . . . . . 6 ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) β†’ ((𝐴𝐷𝐡)𝐺𝐡) = 𝐴)
14133expb 1120 . . . . 5 ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((𝐴𝐷𝐡)𝐺𝐡) = 𝐴)
15143ad2antl1 1185 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((𝐴𝐷𝐡)𝐺𝐡) = 𝐴)
1615fveq2d 6895 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜((𝐴𝐷𝐡)𝐺𝐡)) = (πΉβ€˜π΄))
172, 12grpodivcl 29787 . . . . . . 7 ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋) β†’ (𝐴𝐷𝐡) ∈ 𝑋)
18173expb 1120 . . . . . 6 ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (𝐴𝐷𝐡) ∈ 𝑋)
19 simprr 771 . . . . . 6 ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ 𝐡 ∈ 𝑋)
2018, 19jca 512 . . . . 5 ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((𝐴𝐷𝐡) ∈ 𝑋 ∧ 𝐡 ∈ 𝑋))
21203ad2antl1 1185 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((𝐴𝐷𝐡) ∈ 𝑋 ∧ 𝐡 ∈ 𝑋))
222ghomlinOLD 36751 . . . . 5 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ ((𝐴𝐷𝐡) ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((πΉβ€˜(𝐴𝐷𝐡))𝐻(πΉβ€˜π΅)) = (πΉβ€˜((𝐴𝐷𝐡)𝐺𝐡)))
2322eqcomd 2738 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ ((𝐴𝐷𝐡) ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜((𝐴𝐷𝐡)𝐺𝐡)) = ((πΉβ€˜(𝐴𝐷𝐡))𝐻(πΉβ€˜π΅)))
2421, 23syldan 591 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜((𝐴𝐷𝐡)𝐺𝐡)) = ((πΉβ€˜(𝐴𝐷𝐡))𝐻(πΉβ€˜π΅)))
2511, 16, 243eqtr2rd 2779 . 2 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((πΉβ€˜(𝐴𝐷𝐡))𝐻(πΉβ€˜π΅)) = (((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))𝐻(πΉβ€˜π΅)))
26183ad2antl1 1185 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (𝐴𝐷𝐡) ∈ 𝑋)
274ffvelcdmda 7086 . . . 4 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴𝐷𝐡) ∈ 𝑋) β†’ (πΉβ€˜(𝐴𝐷𝐡)) ∈ ran 𝐻)
2826, 27syldan 591 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜(𝐴𝐷𝐡)) ∈ ran 𝐻)
293, 9grpodivcl 29787 . . . 4 ((𝐻 ∈ GrpOp ∧ (πΉβ€˜π΄) ∈ ran 𝐻 ∧ (πΉβ€˜π΅) ∈ ran 𝐻) β†’ ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅)) ∈ ran 𝐻)
301, 6, 8, 29syl3anc 1371 . . 3 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅)) ∈ ran 𝐻)
313grporcan 29766 . . 3 ((𝐻 ∈ GrpOp ∧ ((πΉβ€˜(𝐴𝐷𝐡)) ∈ ran 𝐻 ∧ ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅)) ∈ ran 𝐻 ∧ (πΉβ€˜π΅) ∈ ran 𝐻)) β†’ (((πΉβ€˜(𝐴𝐷𝐡))𝐻(πΉβ€˜π΅)) = (((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))𝐻(πΉβ€˜π΅)) ↔ (πΉβ€˜(𝐴𝐷𝐡)) = ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))))
321, 28, 30, 8, 31syl13anc 1372 . 2 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (((πΉβ€˜(𝐴𝐷𝐡))𝐻(πΉβ€˜π΅)) = (((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))𝐻(πΉβ€˜π΅)) ↔ (πΉβ€˜(𝐴𝐷𝐡)) = ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅))))
3325, 32mpbid 231 1 (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋)) β†’ (πΉβ€˜(𝐴𝐷𝐡)) = ((πΉβ€˜π΄)𝐢(πΉβ€˜π΅)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ran crn 5677  β€˜cfv 6543  (class class class)co 7408  GrpOpcgr 29737   /𝑔 cgs 29740   GrpOpHom cghomOLD 36746
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 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  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-ral 3062  df-rex 3071  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-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  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-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-grpo 29741  df-gid 29742  df-ginv 29743  df-gdiv 29744  df-ghomOLD 36747
This theorem is referenced by:  grpokerinj  36756  rngohomsub  36836
  Copyright terms: Public domain W3C validator