pwspjmhmmgpd

Description: The projection given by pwspjmhm is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024)

	Ref	Expression
Hypotheses	pwspjmhmmgpd.y	$⊢ Y = R ↑_{𝑠} I$
	pwspjmhmmgpd.b	$⊢ B = {Base}_{Y}$
	pwspjmhmmgpd.m	$⊢ M = {mulGrp}_{Y}$
	pwspjmhmmgpd.t	$⊢ T = {mulGrp}_{R}$
	pwspjmhmmgpd.r	$⊢ φ \to R \in Ring$
	pwspjmhmmgpd.i	$⊢ φ \to I \in V$
	pwspjmhmmgpd.a	$⊢ φ \to A \in I$
Assertion	pwspjmhmmgpd	$⊢ φ \to (x \in B ⟼ x (A)) \in (M MndHom T)$

Proof

Step	Hyp	Ref	Expression
1		pwspjmhmmgpd.y	$⊢ Y = R ↑_{𝑠} I$
2		pwspjmhmmgpd.b	$⊢ B = {Base}_{Y}$
3		pwspjmhmmgpd.m	$⊢ M = {mulGrp}_{Y}$
4		pwspjmhmmgpd.t	$⊢ T = {mulGrp}_{R}$
5		pwspjmhmmgpd.r	$⊢ φ \to R \in Ring$
6		pwspjmhmmgpd.i	$⊢ φ \to I \in V$
7		pwspjmhmmgpd.a	$⊢ φ \to A \in I$
8	3 2	mgpbas	$⊢ B = {Base}_{M}$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	4 9	mgpbas	$⊢ {Base}_{R} = {Base}_{T}$
11		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
12	3 11	mgpplusg	$⊢ \cdot_{Y} = +_{M}$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	4 13	mgpplusg	$⊢ \cdot_{R} = +_{T}$
15		eqid	$⊢ 1_{Y} = 1_{Y}$
16	3 15	ringidval	$⊢ 1_{Y} = 0_{M}$
17		eqid	$⊢ 1_{R} = 1_{R}$
18	4 17	ringidval	$⊢ 1_{R} = 0_{T}$
19	1	pwsring	$⊢ (R \in Ring \land I \in V) \to Y \in Ring$
20	5 6 19	syl2anc	$⊢ φ \to Y \in Ring$
21	3	ringmgp	$⊢ Y \in Ring \to M \in Mnd$
22	20 21	syl	$⊢ φ \to M \in Mnd$
23	4	ringmgp	$⊢ R \in Ring \to T \in Mnd$
24	5 23	syl	$⊢ φ \to T \in Mnd$
25	5	adantr	$⊢ (φ \land x \in B) \to R \in Ring$
26	6	adantr	$⊢ (φ \land x \in B) \to I \in V$
27		simpr	$⊢ (φ \land x \in B) \to x \in B$
28	1 9 2 25 26 27	pwselbas	$⊢ (φ \land x \in B) \to x : I ⟶ {Base}_{R}$
29	7	adantr	$⊢ (φ \land x \in B) \to A \in I$
30	28 29	ffvelrnd	$⊢ (φ \land x \in B) \to x (A) \in {Base}_{R}$
31	30	fmpttd	$⊢ φ \to (x \in B ⟼ x (A)) : B ⟶ {Base}_{R}$
32	5	adantr	$⊢ (φ \land (a \in B \land b \in B)) \to R \in Ring$
33	6	adantr	$⊢ (φ \land (a \in B \land b \in B)) \to I \in V$
34		simprl	$⊢ (φ \land (a \in B \land b \in B)) \to a \in B$
35		simprr	$⊢ (φ \land (a \in B \land b \in B)) \to b \in B$
36	1 2 32 33 34 35 13 11	pwsmulrval	$⊢ (φ \land (a \in B \land b \in B)) \to a \cdot_{Y} b = a {\cdot_{R}}_{f} b$
37	36	fveq1d	$⊢ (φ \land (a \in B \land b \in B)) \to (a \cdot_{Y} b) (A) = (a {\cdot_{R}}_{f} b) (A)$
38	1 9 2 32 33 34	pwselbas	$⊢ (φ \land (a \in B \land b \in B)) \to a : I ⟶ {Base}_{R}$
39	38	ffnd	$⊢ (φ \land (a \in B \land b \in B)) \to a Fn I$
40	1 9 2 32 33 35	pwselbas	$⊢ (φ \land (a \in B \land b \in B)) \to b : I ⟶ {Base}_{R}$
41	40	ffnd	$⊢ (φ \land (a \in B \land b \in B)) \to b Fn I$
42		inidm	$⊢ I \cap I = I$
43		eqidd	$⊢ ((φ \land (a \in B \land b \in B)) \land A \in I) \to a (A) = a (A)$
44		eqidd	$⊢ ((φ \land (a \in B \land b \in B)) \land A \in I) \to b (A) = b (A)$
45	39 41 33 33 42 43 44	ofval	$⊢ ((φ \land (a \in B \land b \in B)) \land A \in I) \to (a {\cdot_{R}}_{f} b) (A) = a (A) \cdot_{R} b (A)$
46	7 45	mpidan	$⊢ (φ \land (a \in B \land b \in B)) \to (a {\cdot_{R}}_{f} b) (A) = a (A) \cdot_{R} b (A)$
47	37 46	eqtrd	$⊢ (φ \land (a \in B \land b \in B)) \to (a \cdot_{Y} b) (A) = a (A) \cdot_{R} b (A)$
48	2 11	ringcl	$⊢ (Y \in Ring \land a \in B \land b \in B) \to a \cdot_{Y} b \in B$
49	20 48	syl3an1	$⊢ (φ \land a \in B \land b \in B) \to a \cdot_{Y} b \in B$
50	49	3expb	$⊢ (φ \land (a \in B \land b \in B)) \to a \cdot_{Y} b \in B$
51		fveq1	$⊢ x = a \cdot_{Y} b \to x (A) = (a \cdot_{Y} b) (A)$
52		eqid	$⊢ (x \in B ⟼ x (A)) = (x \in B ⟼ x (A))$
53		fvex	$⊢ (a \cdot_{Y} b) (A) \in V$
54	51 52 53	fvmpt	$⊢ a \cdot_{Y} b \in B \to (x \in B ⟼ x (A)) (a \cdot_{Y} b) = (a \cdot_{Y} b) (A)$
55	50 54	syl	$⊢ (φ \land (a \in B \land b \in B)) \to (x \in B ⟼ x (A)) (a \cdot_{Y} b) = (a \cdot_{Y} b) (A)$
56		fveq1	$⊢ x = a \to x (A) = a (A)$
57		fvex	$⊢ a (A) \in V$
58	56 52 57	fvmpt	$⊢ a \in B \to (x \in B ⟼ x (A)) (a) = a (A)$
59	34 58	syl	$⊢ (φ \land (a \in B \land b \in B)) \to (x \in B ⟼ x (A)) (a) = a (A)$
60		fveq1	$⊢ x = b \to x (A) = b (A)$
61		fvex	$⊢ b (A) \in V$
62	60 52 61	fvmpt	$⊢ b \in B \to (x \in B ⟼ x (A)) (b) = b (A)$
63	35 62	syl	$⊢ (φ \land (a \in B \land b \in B)) \to (x \in B ⟼ x (A)) (b) = b (A)$
64	59 63	oveq12d	$⊢ (φ \land (a \in B \land b \in B)) \to (x \in B ⟼ x (A)) (a) \cdot_{R} (x \in B ⟼ x (A)) (b) = a (A) \cdot_{R} b (A)$
65	47 55 64	3eqtr4d	$⊢ (φ \land (a \in B \land b \in B)) \to (x \in B ⟼ x (A)) (a \cdot_{Y} b) = (x \in B ⟼ x (A)) (a) \cdot_{R} (x \in B ⟼ x (A)) (b)$
66	2 15	ringidcl	$⊢ Y \in Ring \to 1_{Y} \in B$
67		fveq1	$⊢ x = 1_{Y} \to x (A) = 1_{Y} (A)$
68		fvex	$⊢ 1_{Y} (A) \in V$
69	67 52 68	fvmpt	$⊢ 1_{Y} \in B \to (x \in B ⟼ x (A)) (1_{Y}) = 1_{Y} (A)$
70	20 66 69	3syl	$⊢ φ \to (x \in B ⟼ x (A)) (1_{Y}) = 1_{Y} (A)$
71	1 17	pws1	$⊢ (R \in Ring \land I \in V) \to I \times \{1_{R}\} = 1_{Y}$
72	5 6 71	syl2anc	$⊢ φ \to I \times \{1_{R}\} = 1_{Y}$
73	72	fveq1d	$⊢ φ \to (I \times \{1_{R}\}) (A) = 1_{Y} (A)$
74		fvex	$⊢ 1_{R} \in V$
75	74	fvconst2	$⊢ A \in I \to (I \times \{1_{R}\}) (A) = 1_{R}$
76	7 75	syl	$⊢ φ \to (I \times \{1_{R}\}) (A) = 1_{R}$
77	70 73 76	3eqtr2d	$⊢ φ \to (x \in B ⟼ x (A)) (1_{Y}) = 1_{R}$
78	8 10 12 14 16 18 22 24 31 65 77	ismhmd	$⊢ φ \to (x \in B ⟼ x (A)) \in (M MndHom T)$

Metamath Proof Explorer

Theorem pwspjmhmmgpd

Proof