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	$⊢ \underset{˙}{∙} = \cdot_{Y}$
	pwsmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	pwsmulg	$⊢ ((R \in Mnd \land I \in V) \land (N \in ℕ_{0} \land X \in B \land A \in I)) \to (N \underset{˙}{∙} X) (A) = N \underset{˙}{\cdot} X (A)$

Proof

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

Metamath Proof Explorer

Theorem pwsmulg

Proof