Metamath Proof Explorer

Theorem pwsmulg

Description: Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses pwsmulg.y ⊢ Y = R ↑ 𝑠 I
pwsmulg.b ⊢ B = Base Y
pwsmulg.s ⊢ ∙ ˙ = ⋅ Y
pwsmulg.t ⊢ · ˙ = ⋅ R
Assertion pwsmulg ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → N ∙ ˙ X ⁡ A = N · ˙ X ⁡ A

Proof

Step Hyp Ref Expression
1 pwsmulg.y ⊢ Y = R ↑ 𝑠 I
2 pwsmulg.b ⊢ B = Base Y
3 pwsmulg.s ⊢ ∙ ˙ = ⋅ Y
4 pwsmulg.t ⊢ · ˙ = ⋅ R
5 simpll ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → R ∈ Mnd
6 simplr ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → I ∈ V
7 simpr3 ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → A ∈ I
8 1 2 pwspjmhm ⊢ R ∈ Mnd ∧ I ∈ V ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ∈ Y MndHom R
9 5 6 7 8 syl3anc ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ∈ Y MndHom R
10 simpr1 ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → N ∈ ℕ 0
11 simpr2 ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → X ∈ B
12 2 3 4 mhmmulg ⊢ x ∈ B ⟼ x ⁡ A ∈ Y MndHom R ∧ N ∈ ℕ 0 ∧ X ∈ B → x ∈ B ⟼ x ⁡ A ⁡ N ∙ ˙ X = N · ˙ x ∈ B ⟼ x ⁡ A ⁡ X
13 9 10 11 12 syl3anc ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ⁡ N ∙ ˙ X = N · ˙ x ∈ B ⟼ x ⁡ A ⁡ X
14 1 pwsmnd ⊢ R ∈ Mnd ∧ I ∈ V → Y ∈ Mnd
15 14 adantr ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → Y ∈ Mnd
16 2 3 15 10 11 mulgnn0cld ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → N ∙ ˙ X ∈ B
17 fveq1 ⊢ x = N ∙ ˙ X → x ⁡ A = N ∙ ˙ X ⁡ A
18 eqid ⊢ x ∈ B ⟼ x ⁡ A = x ∈ B ⟼ x ⁡ A
19 fvex ⊢ N ∙ ˙ X ⁡ A ∈ V
20 17 18 19 fvmpt ⊢ N ∙ ˙ X ∈ B → x ∈ B ⟼ x ⁡ A ⁡ N ∙ ˙ X = N ∙ ˙ X ⁡ A
21 16 20 syl ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ⁡ N ∙ ˙ X = N ∙ ˙ X ⁡ A
22 fveq1 ⊢ x = X → x ⁡ A = X ⁡ A
23 fvex ⊢ X ⁡ A ∈ V
24 22 18 23 fvmpt ⊢ X ∈ B → x ∈ B ⟼ x ⁡ A ⁡ X = X ⁡ A
25 11 24 syl ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → x ∈ B ⟼ x ⁡ A ⁡ X = X ⁡ A
26 25 oveq2d ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → N · ˙ x ∈ B ⟼ x ⁡ A ⁡ X = N · ˙ X ⁡ A
27 13 21 26 3eqtr3d ⊢ R ∈ Mnd ∧ I ∈ V ∧ N ∈ ℕ 0 ∧ X ∈ B ∧ A ∈ I → N ∙ ˙ X ⁡ A = N · ˙ X ⁡ A