pwspjmhm

Description: A projection from a structure power of a monoid to the monoid itself is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	pwspjmhm.y	$⊢ Y = R ↑_{𝑠} I$
	pwspjmhm.b	$⊢ B = {Base}_{Y}$
Assertion	pwspjmhm	$⊢ (R \in Mnd \land I \in V \land A \in I) \to (x \in B ⟼ x (A)) \in (Y MndHom R)$

Proof

Step	Hyp	Ref	Expression
1		pwspjmhm.y	$⊢ Y = R ↑_{𝑠} I$
2		pwspjmhm.b	$⊢ B = {Base}_{Y}$
3		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
4		eqid	$⊢ {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
5		simp2	$⊢ (R \in Mnd \land I \in V \land A \in I) \to I \in V$
6		fvexd	$⊢ (R \in Mnd \land I \in V \land A \in I) \to Scalar (R) \in V$
7		fconst6g	$⊢ R \in Mnd \to (I \times \{R\}) : I ⟶ Mnd$
8	7	3ad2ant1	$⊢ (R \in Mnd \land I \in V \land A \in I) \to (I \times \{R\}) : I ⟶ Mnd$
9		simp3	$⊢ (R \in Mnd \land I \in V \land A \in I) \to A \in I$
10	3 4 5 6 8 9	prdspjmhm	$⊢ (R \in Mnd \land I \in V \land A \in I) \to (x \in {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} ⟼ x (A)) \in ((Scalar (R) ⨉_{𝑠} (I \times \{R\})) MndHom (I \times \{R\}) (A))$
11		eqid	$⊢ Scalar (R) = Scalar (R)$
12	1 11	pwsval	$⊢ (R \in Mnd \land I \in V) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
13	12	3adant3	$⊢ (R \in Mnd \land I \in V \land A \in I) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
14	13	fveq2d	$⊢ (R \in Mnd \land I \in V \land A \in I) \to {Base}_{Y} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
15	2 14	eqtrid	$⊢ (R \in Mnd \land I \in V \land A \in I) \to B = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
16	15	mpteq1d	$⊢ (R \in Mnd \land I \in V \land A \in I) \to (x \in B ⟼ x (A)) = (x \in {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} ⟼ x (A))$
17		fvconst2g	$⊢ (R \in Mnd \land A \in I) \to (I \times \{R\}) (A) = R$
18	17	3adant2	$⊢ (R \in Mnd \land I \in V \land A \in I) \to (I \times \{R\}) (A) = R$
19	18	eqcomd	$⊢ (R \in Mnd \land I \in V \land A \in I) \to R = (I \times \{R\}) (A)$
20	13 19	oveq12d	$⊢ (R \in Mnd \land I \in V \land A \in I) \to Y MndHom R = (Scalar (R) ⨉_{𝑠} (I \times \{R\})) MndHom (I \times \{R\}) (A)$
21	10 16 20	3eltr4d	$⊢ (R \in Mnd \land I \in V \land A \in I) \to (x \in B ⟼ x (A)) \in (Y MndHom R)$

Metamath Proof Explorer

Theorem pwspjmhm

Proof