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	mulgnn0cl	$⊢ (Y \in Mnd \land N \in ℕ_{0} \land X \in B) \to N \underset{˙}{∙} X \in B$
17	15 10 11 16	syl3anc	$⊢ ((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$
18		fveq1	$⊢ x = N \underset{˙}{∙} X \to x (A) = (N \underset{˙}{∙} X) (A)$
19		eqid	$⊢ (x \in B ⟼ x (A)) = (x \in B ⟼ x (A))$
20		fvex	$⊢ (N \underset{˙}{∙} X) (A) \in V$
21	18 19 20	fvmpt	$⊢ N \underset{˙}{∙} X \in B \to (x \in B ⟼ x (A)) (N \underset{˙}{∙} X) = (N \underset{˙}{∙} X) (A)$
22	17 21	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)$
23		fveq1	$⊢ x = X \to x (A) = X (A)$
24		fvex	$⊢ X (A) \in V$
25	23 19 24	fvmpt	$⊢ X \in B \to (x \in B ⟼ x (A)) (X) = X (A)$
26	11 25	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)$
27	26	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)$
28	13 22 27	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