Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwsco2rhm Structured version   Visualization version   GIF version

Theorem pwsco2rhm 18941
 Description: Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
Hypotheses
Ref Expression
pwsco2rhm.y 𝑌 = (𝑅s 𝐴)
pwsco2rhm.z 𝑍 = (𝑆s 𝐴)
pwsco2rhm.b 𝐵 = (Base‘𝑌)
pwsco2rhm.a (𝜑𝐴𝑉)
pwsco2rhm.f (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
Assertion
Ref Expression
pwsco2rhm (𝜑 → (𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 RingHom 𝑍))
Distinct variable groups:   𝐴,𝑔   𝜑,𝑔   𝑅,𝑔   𝑆,𝑔   𝑔,𝑌   𝐵,𝑔   𝑔,𝐹   𝑔,𝑍
Allowed substitution hint:   𝑉(𝑔)

Proof of Theorem pwsco2rhm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwsco2rhm.f . . . . 5 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
2 rhmrcl1 18921 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring)
31, 2syl 17 . . . 4 (𝜑𝑅 ∈ Ring)
4 pwsco2rhm.a . . . 4 (𝜑𝐴𝑉)
5 pwsco2rhm.y . . . . 5 𝑌 = (𝑅s 𝐴)
65pwsring 18815 . . . 4 ((𝑅 ∈ Ring ∧ 𝐴𝑉) → 𝑌 ∈ Ring)
73, 4, 6syl2anc 696 . . 3 (𝜑𝑌 ∈ Ring)
8 rhmrcl2 18922 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring)
91, 8syl 17 . . . 4 (𝜑𝑆 ∈ Ring)
10 pwsco2rhm.z . . . . 5 𝑍 = (𝑆s 𝐴)
1110pwsring 18815 . . . 4 ((𝑆 ∈ Ring ∧ 𝐴𝑉) → 𝑍 ∈ Ring)
129, 4, 11syl2anc 696 . . 3 (𝜑𝑍 ∈ Ring)
137, 12jca 555 . 2 (𝜑 → (𝑌 ∈ Ring ∧ 𝑍 ∈ Ring))
14 pwsco2rhm.b . . . . 5 𝐵 = (Base‘𝑌)
15 rhmghm 18927 . . . . . . 7 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
161, 15syl 17 . . . . . 6 (𝜑𝐹 ∈ (𝑅 GrpHom 𝑆))
17 ghmmhm 17871 . . . . . 6 (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹 ∈ (𝑅 MndHom 𝑆))
1816, 17syl 17 . . . . 5 (𝜑𝐹 ∈ (𝑅 MndHom 𝑆))
195, 10, 14, 4, 18pwsco2mhm 17572 . . . 4 (𝜑 → (𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 MndHom 𝑍))
20 ringgrp 18752 . . . . . 6 (𝑌 ∈ Ring → 𝑌 ∈ Grp)
217, 20syl 17 . . . . 5 (𝜑𝑌 ∈ Grp)
22 ringgrp 18752 . . . . . 6 (𝑍 ∈ Ring → 𝑍 ∈ Grp)
2312, 22syl 17 . . . . 5 (𝜑𝑍 ∈ Grp)
24 ghmmhmb 17872 . . . . 5 ((𝑌 ∈ Grp ∧ 𝑍 ∈ Grp) → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍))
2521, 23, 24syl2anc 696 . . . 4 (𝜑 → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍))
2619, 25eleqtrrd 2842 . . 3 (𝜑 → (𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 GrpHom 𝑍))
27 eqid 2760 . . . . 5 ((mulGrp‘𝑅) ↑s 𝐴) = ((mulGrp‘𝑅) ↑s 𝐴)
28 eqid 2760 . . . . 5 ((mulGrp‘𝑆) ↑s 𝐴) = ((mulGrp‘𝑆) ↑s 𝐴)
29 eqid 2760 . . . . 5 (Base‘((mulGrp‘𝑅) ↑s 𝐴)) = (Base‘((mulGrp‘𝑅) ↑s 𝐴))
30 eqid 2760 . . . . . . 7 (mulGrp‘𝑅) = (mulGrp‘𝑅)
31 eqid 2760 . . . . . . 7 (mulGrp‘𝑆) = (mulGrp‘𝑆)
3230, 31rhmmhm 18924 . . . . . 6 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))
331, 32syl 17 . . . . 5 (𝜑𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))
3427, 28, 29, 4, 33pwsco2mhm 17572 . . . 4 (𝜑 → (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s 𝐴)) ↦ (𝐹𝑔)) ∈ (((mulGrp‘𝑅) ↑s 𝐴) MndHom ((mulGrp‘𝑆) ↑s 𝐴)))
35 eqid 2760 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
365, 35pwsbas 16349 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐴𝑉) → ((Base‘𝑅) ↑𝑚 𝐴) = (Base‘𝑌))
373, 4, 36syl2anc 696 . . . . . . 7 (𝜑 → ((Base‘𝑅) ↑𝑚 𝐴) = (Base‘𝑌))
3837, 14syl6eqr 2812 . . . . . 6 (𝜑 → ((Base‘𝑅) ↑𝑚 𝐴) = 𝐵)
3930ringmgp 18753 . . . . . . . 8 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
403, 39syl 17 . . . . . . 7 (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
4130, 35mgpbas 18695 . . . . . . . 8 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
4227, 41pwsbas 16349 . . . . . . 7 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐴𝑉) → ((Base‘𝑅) ↑𝑚 𝐴) = (Base‘((mulGrp‘𝑅) ↑s 𝐴)))
4340, 4, 42syl2anc 696 . . . . . 6 (𝜑 → ((Base‘𝑅) ↑𝑚 𝐴) = (Base‘((mulGrp‘𝑅) ↑s 𝐴)))
4438, 43eqtr3d 2796 . . . . 5 (𝜑𝐵 = (Base‘((mulGrp‘𝑅) ↑s 𝐴)))
4544mpteq1d 4890 . . . 4 (𝜑 → (𝑔𝐵 ↦ (𝐹𝑔)) = (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s 𝐴)) ↦ (𝐹𝑔)))
46 eqidd 2761 . . . . 5 (𝜑 → (Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌)))
47 eqidd 2761 . . . . 5 (𝜑 → (Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍)))
48 eqid 2760 . . . . . . . 8 (mulGrp‘𝑌) = (mulGrp‘𝑌)
49 eqid 2760 . . . . . . . 8 (Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))
50 eqid 2760 . . . . . . . 8 (+g‘(mulGrp‘𝑌)) = (+g‘(mulGrp‘𝑌))
51 eqid 2760 . . . . . . . 8 (+g‘((mulGrp‘𝑅) ↑s 𝐴)) = (+g‘((mulGrp‘𝑅) ↑s 𝐴))
525, 30, 27, 48, 49, 29, 50, 51pwsmgp 18818 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐴𝑉) → ((Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s 𝐴)) ∧ (+g‘(mulGrp‘𝑌)) = (+g‘((mulGrp‘𝑅) ↑s 𝐴))))
533, 4, 52syl2anc 696 . . . . . 6 (𝜑 → ((Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s 𝐴)) ∧ (+g‘(mulGrp‘𝑌)) = (+g‘((mulGrp‘𝑅) ↑s 𝐴))))
5453simpld 477 . . . . 5 (𝜑 → (Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s 𝐴)))
55 eqid 2760 . . . . . . . 8 (mulGrp‘𝑍) = (mulGrp‘𝑍)
56 eqid 2760 . . . . . . . 8 (Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍))
57 eqid 2760 . . . . . . . 8 (Base‘((mulGrp‘𝑆) ↑s 𝐴)) = (Base‘((mulGrp‘𝑆) ↑s 𝐴))
58 eqid 2760 . . . . . . . 8 (+g‘(mulGrp‘𝑍)) = (+g‘(mulGrp‘𝑍))
59 eqid 2760 . . . . . . . 8 (+g‘((mulGrp‘𝑆) ↑s 𝐴)) = (+g‘((mulGrp‘𝑆) ↑s 𝐴))
6010, 31, 28, 55, 56, 57, 58, 59pwsmgp 18818 . . . . . . 7 ((𝑆 ∈ Ring ∧ 𝐴𝑉) → ((Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s 𝐴)) ∧ (+g‘(mulGrp‘𝑍)) = (+g‘((mulGrp‘𝑆) ↑s 𝐴))))
619, 4, 60syl2anc 696 . . . . . 6 (𝜑 → ((Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s 𝐴)) ∧ (+g‘(mulGrp‘𝑍)) = (+g‘((mulGrp‘𝑆) ↑s 𝐴))))
6261simpld 477 . . . . 5 (𝜑 → (Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s 𝐴)))
6353simprd 482 . . . . . 6 (𝜑 → (+g‘(mulGrp‘𝑌)) = (+g‘((mulGrp‘𝑅) ↑s 𝐴)))
6463oveqdr 6837 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘((mulGrp‘𝑅) ↑s 𝐴))𝑦))
6561simprd 482 . . . . . 6 (𝜑 → (+g‘(mulGrp‘𝑍)) = (+g‘((mulGrp‘𝑆) ↑s 𝐴)))
6665oveqdr 6837 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑍)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑍)))) → (𝑥(+g‘(mulGrp‘𝑍))𝑦) = (𝑥(+g‘((mulGrp‘𝑆) ↑s 𝐴))𝑦))
6746, 47, 54, 62, 64, 66mhmpropd 17542 . . . 4 (𝜑 → ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)) = (((mulGrp‘𝑅) ↑s 𝐴) MndHom ((mulGrp‘𝑆) ↑s 𝐴)))
6834, 45, 673eltr4d 2854 . . 3 (𝜑 → (𝑔𝐵 ↦ (𝐹𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)))
6926, 68jca 555 . 2 (𝜑 → ((𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔𝐵 ↦ (𝐹𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))))
7048, 55isrhm 18923 . 2 ((𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 RingHom 𝑍) ↔ ((𝑌 ∈ Ring ∧ 𝑍 ∈ Ring) ∧ ((𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔𝐵 ↦ (𝐹𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)))))
7113, 69, 70sylanbrc 701 1 (𝜑 → (𝑔𝐵 ↦ (𝐹𝑔)) ∈ (𝑌 RingHom 𝑍))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ↦ cmpt 4881   ∘ ccom 5270  ‘cfv 6049  (class class class)co 6813   ↑𝑚 cmap 8023  Basecbs 16059  +gcplusg 16143   ↑s cpws 16309  Mndcmnd 17495   MndHom cmhm 17534  Grpcgrp 17623   GrpHom cghm 17858  mulGrpcmgp 18689  Ringcrg 18747   RingHom crh 18914 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-fz 12520  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-plusg 16156  df-mulr 16157  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-hom 16168  df-cco 16169  df-0g 16304  df-prds 16310  df-pws 16312  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-grp 17626  df-minusg 17627  df-ghm 17859  df-mgp 18690  df-ur 18702  df-ring 18749  df-rnghom 18917 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator