Metamath Proof Explorer


Theorem pwsco1rhm

Description: Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco1rhm.y Y = R 𝑠 A
pwsco1rhm.z Z = R 𝑠 B
pwsco1rhm.c C = Base Z
pwsco1rhm.r φ R Ring
pwsco1rhm.a φ A V
pwsco1rhm.b φ B W
pwsco1rhm.f φ F : A B
Assertion pwsco1rhm φ g C g F Z RingHom Y

Proof

Step Hyp Ref Expression
1 pwsco1rhm.y Y = R 𝑠 A
2 pwsco1rhm.z Z = R 𝑠 B
3 pwsco1rhm.c C = Base Z
4 pwsco1rhm.r φ R Ring
5 pwsco1rhm.a φ A V
6 pwsco1rhm.b φ B W
7 pwsco1rhm.f φ F : A B
8 2 pwsring R Ring B W Z Ring
9 4 6 8 syl2anc φ Z Ring
10 1 pwsring R Ring A V Y Ring
11 4 5 10 syl2anc φ Y Ring
12 ringmnd R Ring R Mnd
13 4 12 syl φ R Mnd
14 1 2 3 13 5 6 7 pwsco1mhm φ g C g F Z MndHom Y
15 ringgrp Z Ring Z Grp
16 9 15 syl φ Z Grp
17 ringgrp Y Ring Y Grp
18 11 17 syl φ Y Grp
19 ghmmhmb Z Grp Y Grp Z GrpHom Y = Z MndHom Y
20 16 18 19 syl2anc φ Z GrpHom Y = Z MndHom Y
21 14 20 eleqtrrd φ g C g F Z GrpHom Y
22 eqid mulGrp R 𝑠 A = mulGrp R 𝑠 A
23 eqid mulGrp R 𝑠 B = mulGrp R 𝑠 B
24 eqid Base mulGrp R 𝑠 B = Base mulGrp R 𝑠 B
25 eqid mulGrp R = mulGrp R
26 25 ringmgp R Ring mulGrp R Mnd
27 4 26 syl φ mulGrp R Mnd
28 22 23 24 27 5 6 7 pwsco1mhm φ g Base mulGrp R 𝑠 B g F mulGrp R 𝑠 B MndHom mulGrp R 𝑠 A
29 eqid Base R = Base R
30 2 29 pwsbas R Mnd B W Base R B = Base Z
31 13 6 30 syl2anc φ Base R B = Base Z
32 31 3 eqtr4di φ Base R B = C
33 25 29 mgpbas Base R = Base mulGrp R
34 23 33 pwsbas mulGrp R Mnd B W Base R B = Base mulGrp R 𝑠 B
35 27 6 34 syl2anc φ Base R B = Base mulGrp R 𝑠 B
36 32 35 eqtr3d φ C = Base mulGrp R 𝑠 B
37 36 mpteq1d φ g C g F = g Base mulGrp R 𝑠 B g F
38 eqidd φ Base mulGrp Z = Base mulGrp Z
39 eqidd φ Base mulGrp Y = Base mulGrp Y
40 eqid mulGrp Z = mulGrp Z
41 eqid Base mulGrp Z = Base mulGrp Z
42 eqid + mulGrp Z = + mulGrp Z
43 eqid + mulGrp R 𝑠 B = + mulGrp R 𝑠 B
44 2 25 23 40 41 24 42 43 pwsmgp R Ring B W Base mulGrp Z = Base mulGrp R 𝑠 B + mulGrp Z = + mulGrp R 𝑠 B
45 4 6 44 syl2anc φ Base mulGrp Z = Base mulGrp R 𝑠 B + mulGrp Z = + mulGrp R 𝑠 B
46 45 simpld φ Base mulGrp Z = Base mulGrp R 𝑠 B
47 eqid mulGrp Y = mulGrp Y
48 eqid Base mulGrp Y = Base mulGrp Y
49 eqid Base mulGrp R 𝑠 A = Base mulGrp R 𝑠 A
50 eqid + mulGrp Y = + mulGrp Y
51 eqid + mulGrp R 𝑠 A = + mulGrp R 𝑠 A
52 1 25 22 47 48 49 50 51 pwsmgp R Ring A V Base mulGrp Y = Base mulGrp R 𝑠 A + mulGrp Y = + mulGrp R 𝑠 A
53 4 5 52 syl2anc φ Base mulGrp Y = Base mulGrp R 𝑠 A + mulGrp Y = + mulGrp R 𝑠 A
54 53 simpld φ Base mulGrp Y = Base mulGrp R 𝑠 A
55 45 simprd φ + mulGrp Z = + mulGrp R 𝑠 B
56 55 oveqdr φ x Base mulGrp Z y Base mulGrp Z x + mulGrp Z y = x + mulGrp R 𝑠 B y
57 53 simprd φ + mulGrp Y = + mulGrp R 𝑠 A
58 57 oveqdr φ x Base mulGrp Y y Base mulGrp Y x + mulGrp Y y = x + mulGrp R 𝑠 A y
59 38 39 46 54 56 58 mhmpropd φ mulGrp Z MndHom mulGrp Y = mulGrp R 𝑠 B MndHom mulGrp R 𝑠 A
60 28 37 59 3eltr4d φ g C g F mulGrp Z MndHom mulGrp Y
61 21 60 jca φ g C g F Z GrpHom Y g C g F mulGrp Z MndHom mulGrp Y
62 40 47 isrhm g C g F Z RingHom Y Z Ring Y Ring g C g F Z GrpHom Y g C g F mulGrp Z MndHom mulGrp Y
63 9 11 61 62 syl21anbrc φ g C g F Z RingHom Y