pwsvscaval

Description: Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsvscaval.y	$⊢ Y = R ↑_{𝑠} I$
	pwsvscaval.b	$⊢ B = {Base}_{Y}$
	pwsvscaval.s	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	pwsvscaval.t	$⊢ \underset{˙}{∙} = \cdot_{Y}$
	pwsvscaval.f	$⊢ F = Scalar (R)$
	pwsvscaval.k	$⊢ K = {Base}_{F}$
	pwsvscaval.r	$⊢ φ \to R \in V$
	pwsvscaval.i	$⊢ φ \to I \in W$
	pwsvscaval.a	$⊢ φ \to A \in K$
	pwsvscaval.x	$⊢ φ \to X \in B$
	pwsvscaval.j	$⊢ φ \to J \in I$
Assertion	pwsvscaval	$⊢ φ \to (A \underset{˙}{∙} X) (J) = A \underset{˙}{\cdot} X (J)$

Step	Hyp	Ref	Expression
1		pwsvscaval.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsvscaval.b	$⊢ B = {Base}_{Y}$
3		pwsvscaval.s	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		pwsvscaval.t	$⊢ \underset{˙}{∙} = \cdot_{Y}$
5		pwsvscaval.f	$⊢ F = Scalar (R)$
6		pwsvscaval.k	$⊢ K = {Base}_{F}$
7		pwsvscaval.r	$⊢ φ \to R \in V$
8		pwsvscaval.i	$⊢ φ \to I \in W$
9		pwsvscaval.a	$⊢ φ \to A \in K$
10		pwsvscaval.x	$⊢ φ \to X \in B$
11		pwsvscaval.j	$⊢ φ \to J \in I$
12	1 2 3 4 5 6 7 8 9 10	pwsvscafval	$⊢ φ \to A \underset{˙}{∙} X = (I \times \{A\}) {\underset{˙}{\cdot}}_{f} X$
13	12	fveq1d	$⊢ φ \to (A \underset{˙}{∙} X) (J) = ((I \times \{A\}) {\underset{˙}{\cdot}}_{f} X) (J)$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	1 14 2 7 8 10	pwselbas	$⊢ φ \to X : I ⟶ {Base}_{R}$
16	15	ffnd	$⊢ φ \to X Fn I$
17		eqidd	$⊢ (φ \land J \in I) \to X (J) = X (J)$
18	8 9 16 17	ofc1	$⊢ (φ \land J \in I) \to ((I \times \{A\}) {\underset{˙}{\cdot}}_{f} X) (J) = A \underset{˙}{\cdot} X (J)$
19	11 18	mpdan	$⊢ φ \to ((I \times \{A\}) {\underset{˙}{\cdot}}_{f} X) (J) = A \underset{˙}{\cdot} X (J)$
20	13 19	eqtrd	$⊢ φ \to (A \underset{˙}{∙} X) (J) = A \underset{˙}{\cdot} X (J)$

Metamath Proof Explorer