pwsco2rhm

Description: Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pwsco2rhm.y	$⊢ Y = R ↑_{𝑠} A$
	pwsco2rhm.z	$⊢ Z = S ↑_{𝑠} A$
	pwsco2rhm.b	$⊢ B = {Base}_{Y}$
	pwsco2rhm.a	$⊢ φ \to A \in V$
	pwsco2rhm.f	$⊢ φ \to F \in (R RingHom S)$
Assertion	pwsco2rhm	$⊢ φ \to (g \in B ⟼ F \circ g) \in (Y RingHom Z)$

Proof

Step	Hyp	Ref	Expression
1		pwsco2rhm.y	$⊢ Y = R ↑_{𝑠} A$
2		pwsco2rhm.z	$⊢ Z = S ↑_{𝑠} A$
3		pwsco2rhm.b	$⊢ B = {Base}_{Y}$
4		pwsco2rhm.a	$⊢ φ \to A \in V$
5		pwsco2rhm.f	$⊢ φ \to F \in (R RingHom S)$
6		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
7	5 6	syl	$⊢ φ \to R \in Ring$
8	1	pwsring	$⊢ (R \in Ring \land A \in V) \to Y \in Ring$
9	7 4 8	syl2anc	$⊢ φ \to Y \in Ring$
10		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
11	5 10	syl	$⊢ φ \to S \in Ring$
12	2	pwsring	$⊢ (S \in Ring \land A \in V) \to Z \in Ring$
13	11 4 12	syl2anc	$⊢ φ \to Z \in Ring$
14		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
15	5 14	syl	$⊢ φ \to F \in (R GrpHom S)$
16		ghmmhm	$⊢ F \in (R GrpHom S) \to F \in (R MndHom S)$
17	15 16	syl	$⊢ φ \to F \in (R MndHom S)$
18	1 2 3 4 17	pwsco2mhm	$⊢ φ \to (g \in B ⟼ F \circ g) \in (Y MndHom Z)$
19		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
20	9 19	syl	$⊢ φ \to Y \in Grp$
21		ringgrp	$⊢ Z \in Ring \to Z \in Grp$
22	13 21	syl	$⊢ φ \to Z \in Grp$
23		ghmmhmb	$⊢ (Y \in Grp \land Z \in Grp) \to Y GrpHom Z = Y MndHom Z$
24	20 22 23	syl2anc	$⊢ φ \to Y GrpHom Z = Y MndHom Z$
25	18 24	eleqtrrd	$⊢ φ \to (g \in B ⟼ F \circ g) \in (Y GrpHom Z)$
26		eqid	$⊢ {mulGrp}_{R} ↑_{𝑠} A = {mulGrp}_{R} ↑_{𝑠} A$
27		eqid	$⊢ {mulGrp}_{S} ↑_{𝑠} A = {mulGrp}_{S} ↑_{𝑠} A$
28		eqid	$⊢ {Base}_{({mulGrp}_{R} ↑_{𝑠} A)} = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)}$
29		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
30		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
31	29 30	rhmmhm	$⊢ F \in (R RingHom S) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
32	5 31	syl	$⊢ φ \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
33	26 27 28 4 32	pwsco2mhm	$⊢ φ \to (g \in {Base}_{({mulGrp}_{R} ↑_{𝑠} A)} ⟼ F \circ g) \in (({mulGrp}_{R} ↑_{𝑠} A) MndHom ({mulGrp}_{S} ↑_{𝑠} A))$
34		eqid	$⊢ {Base}_{R} = {Base}_{R}$
35	1 34	pwsbas	$⊢ (R \in Ring \land A \in V) \to {Base}_{R}^{A} = {Base}_{Y}$
36	7 4 35	syl2anc	$⊢ φ \to {Base}_{R}^{A} = {Base}_{Y}$
37	36 3	eqtr4di	$⊢ φ \to {Base}_{R}^{A} = B$
38	29	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
39	7 38	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
40	29 34	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
41	26 40	pwsbas	$⊢ ({mulGrp}_{R} \in Mnd \land A \in V) \to {Base}_{R}^{A} = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)}$
42	39 4 41	syl2anc	$⊢ φ \to {Base}_{R}^{A} = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)}$
43	37 42	eqtr3d	$⊢ φ \to B = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)}$
44	43	mpteq1d	$⊢ φ \to (g \in B ⟼ F \circ g) = (g \in {Base}_{({mulGrp}_{R} ↑_{𝑠} A)} ⟼ F \circ g)$
45		eqidd	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
46		eqidd	$⊢ φ \to {Base}_{{mulGrp}_{Z}} = {Base}_{{mulGrp}_{Z}}$
47		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
48		eqid	$⊢ {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
49		eqid	$⊢ +_{{mulGrp}_{Y}} = +_{{mulGrp}_{Y}}$
50		eqid	$⊢ +_{({mulGrp}_{R} ↑_{𝑠} A)} = +_{({mulGrp}_{R} ↑_{𝑠} A)}$
51	1 29 26 47 48 28 49 50	pwsmgp	$⊢ (R \in Ring \land A \in V) \to ({Base}_{{mulGrp}_{Y}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)} \land +_{{mulGrp}_{Y}} = +_{({mulGrp}_{R} ↑_{𝑠} A)})$
52	7 4 51	syl2anc	$⊢ φ \to ({Base}_{{mulGrp}_{Y}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)} \land +_{{mulGrp}_{Y}} = +_{({mulGrp}_{R} ↑_{𝑠} A)})$
53	52	simpld	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} A)}$
54		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
55		eqid	$⊢ {Base}_{{mulGrp}_{Z}} = {Base}_{{mulGrp}_{Z}}$
56		eqid	$⊢ {Base}_{({mulGrp}_{S} ↑_{𝑠} A)} = {Base}_{({mulGrp}_{S} ↑_{𝑠} A)}$
57		eqid	$⊢ +_{{mulGrp}_{Z}} = +_{{mulGrp}_{Z}}$
58		eqid	$⊢ +_{({mulGrp}_{S} ↑_{𝑠} A)} = +_{({mulGrp}_{S} ↑_{𝑠} A)}$
59	2 30 27 54 55 56 57 58	pwsmgp	$⊢ (S \in Ring \land A \in V) \to ({Base}_{{mulGrp}_{Z}} = {Base}_{({mulGrp}_{S} ↑_{𝑠} A)} \land +_{{mulGrp}_{Z}} = +_{({mulGrp}_{S} ↑_{𝑠} A)})$
60	11 4 59	syl2anc	$⊢ φ \to ({Base}_{{mulGrp}_{Z}} = {Base}_{({mulGrp}_{S} ↑_{𝑠} A)} \land +_{{mulGrp}_{Z}} = +_{({mulGrp}_{S} ↑_{𝑠} A)})$
61	60	simpld	$⊢ φ \to {Base}_{{mulGrp}_{Z}} = {Base}_{({mulGrp}_{S} ↑_{𝑠} A)}$
62	52	simprd	$⊢ φ \to +_{{mulGrp}_{Y}} = +_{({mulGrp}_{R} ↑_{𝑠} A)}$
63	62	oveqdr	$⊢ (φ \land (x \in {Base}_{{mulGrp}_{Y}} \land y \in {Base}_{{mulGrp}_{Y}})) \to x +_{{mulGrp}_{Y}} y = x +_{({mulGrp}_{R} ↑_{𝑠} A)} y$
64	60	simprd	$⊢ φ \to +_{{mulGrp}_{Z}} = +_{({mulGrp}_{S} ↑_{𝑠} A)}$
65	64	oveqdr	$⊢ (φ \land (x \in {Base}_{{mulGrp}_{Z}} \land y \in {Base}_{{mulGrp}_{Z}})) \to x +_{{mulGrp}_{Z}} y = x +_{({mulGrp}_{S} ↑_{𝑠} A)} y$
66	45 46 53 61 63 65	mhmpropd	$⊢ φ \to {mulGrp}_{Y} MndHom {mulGrp}_{Z} = ({mulGrp}_{R} ↑_{𝑠} A) MndHom ({mulGrp}_{S} ↑_{𝑠} A)$
67	33 44 66	3eltr4d	$⊢ φ \to (g \in B ⟼ F \circ g) \in ({mulGrp}_{Y} MndHom {mulGrp}_{Z})$
68	25 67	jca	$⊢ φ \to ((g \in B ⟼ F \circ g) \in (Y GrpHom Z) \land (g \in B ⟼ F \circ g) \in ({mulGrp}_{Y} MndHom {mulGrp}_{Z}))$
69	47 54	isrhm	$⊢ (g \in B ⟼ F \circ g) \in (Y RingHom Z) \leftrightarrow ((Y \in Ring \land Z \in Ring) \land ((g \in B ⟼ F \circ g) \in (Y GrpHom Z) \land (g \in B ⟼ F \circ g) \in ({mulGrp}_{Y} MndHom {mulGrp}_{Z})))$
70	9 13 68 69	syl21anbrc	$⊢ φ \to (g \in B ⟼ F \circ g) \in (Y RingHom Z)$

Metamath Proof Explorer

Theorem pwsco2rhm

Proof