Metamath Proof Explorer

Theorem 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 ∈ Mnd ∧ I ∈ V ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ∈ 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 × R = Scalar ⁡ R ⨉ 𝑠 I × R
4 eqid ⊢ Base Scalar ⁡ R ⨉ 𝑠 I × R = Base Scalar ⁡ R ⨉ 𝑠 I × R
5 simp2 ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → I ∈ V
6 fvexd ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → Scalar ⁡ R ∈ V
7 fconst6g ⊢ R ∈ Mnd → I × R : I ⟶ Mnd
8 7 3ad2ant1 ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → I × R : I ⟶ Mnd
9 simp3 ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → A ∈ I
10 3 4 5 6 8 9 prdspjmhm ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → x ∈ Base Scalar ⁡ R ⨉ 𝑠 I × R ⟼ x ⁡ A ∈ Scalar ⁡ R ⨉ 𝑠 I × R MndHom I × R ⁡ A
11 eqid ⊢ Scalar ⁡ R = Scalar ⁡ R
12 1 11 pwsval ⊢ R ∈ Mnd ∧ I ∈ V → Y = Scalar ⁡ R ⨉ 𝑠 I × R
13 12 3adant3 ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → Y = Scalar ⁡ R ⨉ 𝑠 I × R
14 13 fveq2d ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → Base Y = Base Scalar ⁡ R ⨉ 𝑠 I × R
15 2 14 eqtrid ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → B = Base Scalar ⁡ R ⨉ 𝑠 I × R
16 15 mpteq1d ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → x ∈ B ⟼ x ⁡ A = x ∈ Base Scalar ⁡ R ⨉ 𝑠 I × R ⟼ x ⁡ A
17 fvconst2g ⊢ R ∈ Mnd ∧ A ∈ I → I × R ⁡ A = R
18 17 3adant2 ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → I × R ⁡ A = R
19 18 eqcomd ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → R = I × R ⁡ A
20 13 19 oveq12d ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → Y MndHom R = Scalar ⁡ R ⨉ 𝑠 I × R MndHom I × R ⁡ A
21 10 16 20 3eltr4d ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ∈ Y MndHom R