pwsvscafval

Description: Scalar multiplication in a structure power is pointwise. (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$
Assertion	pwsvscafval	$⊢ φ \to A \underset{˙}{∙} X = (I \times \{A\}) {\underset{˙}{\cdot}}_{f} X$

Proof

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	1 5	pwsval	$⊢ (R \in V \land I \in W) \to Y = F ⨉_{𝑠} (I \times \{R\})$
12	7 8 11	syl2anc	$⊢ φ \to Y = F ⨉_{𝑠} (I \times \{R\})$
13	12	fveq2d	$⊢ φ \to \cdot_{Y} = \cdot_{(F ⨉_{𝑠} (I \times \{R\}))}$
14	4 13	syl5eq	$⊢ φ \to \underset{˙}{∙} = \cdot_{(F ⨉_{𝑠} (I \times \{R\}))}$
15	14	oveqd	$⊢ φ \to A \underset{˙}{∙} X = A \cdot_{(F ⨉_{𝑠} (I \times \{R\}))} X$
16		eqid	$⊢ F ⨉_{𝑠} (I \times \{R\}) = F ⨉_{𝑠} (I \times \{R\})$
17		eqid	$⊢ {Base}_{(F ⨉_{𝑠} (I \times \{R\}))} = {Base}_{(F ⨉_{𝑠} (I \times \{R\}))}$
18		eqid	$⊢ \cdot_{(F ⨉_{𝑠} (I \times \{R\}))} = \cdot_{(F ⨉_{𝑠} (I \times \{R\}))}$
19	5	fvexi	$⊢ F \in V$
20	19	a1i	$⊢ φ \to F \in V$
21		fnconstg	$⊢ R \in V \to (I \times \{R\}) Fn I$
22	7 21	syl	$⊢ φ \to (I \times \{R\}) Fn I$
23	12	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(F ⨉_{𝑠} (I \times \{R\}))}$
24	2 23	syl5eq	$⊢ φ \to B = {Base}_{(F ⨉_{𝑠} (I \times \{R\}))}$
25	10 24	eleqtrd	$⊢ φ \to X \in {Base}_{(F ⨉_{𝑠} (I \times \{R\}))}$
26	16 17 18 6 20 8 22 9 25	prdsvscaval	$⊢ φ \to A \cdot_{(F ⨉_{𝑠} (I \times \{R\}))} X = (x \in I ⟼ A \cdot_{(I \times \{R\}) (x)} X (x))$
27		fvconst2g	$⊢ (R \in V \land x \in I) \to (I \times \{R\}) (x) = R$
28	7 27	sylan	$⊢ (φ \land x \in I) \to (I \times \{R\}) (x) = R$
29	28	fveq2d	$⊢ (φ \land x \in I) \to \cdot_{(I \times \{R\}) (x)} = \cdot_{R}$
30	29 3	eqtr4di	$⊢ (φ \land x \in I) \to \cdot_{(I \times \{R\}) (x)} = \underset{˙}{\cdot}$
31	30	oveqd	$⊢ (φ \land x \in I) \to A \cdot_{(I \times \{R\}) (x)} X (x) = A \underset{˙}{\cdot} X (x)$
32	31	mpteq2dva	$⊢ φ \to (x \in I ⟼ A \cdot_{(I \times \{R\}) (x)} X (x)) = (x \in I ⟼ A \underset{˙}{\cdot} X (x))$
33	9	adantr	$⊢ (φ \land x \in I) \to A \in K$
34		fvexd	$⊢ (φ \land x \in I) \to X (x) \in V$
35		fconstmpt	$⊢ I \times \{A\} = (x \in I ⟼ A)$
36	35	a1i	$⊢ φ \to I \times \{A\} = (x \in I ⟼ A)$
37		eqid	$⊢ {Base}_{R} = {Base}_{R}$
38	1 37 2 7 8 10	pwselbas	$⊢ φ \to X : I ⟶ {Base}_{R}$
39	38	feqmptd	$⊢ φ \to X = (x \in I ⟼ X (x))$
40	8 33 34 36 39	offval2	$⊢ φ \to (I \times \{A\}) {\underset{˙}{\cdot}}_{f} X = (x \in I ⟼ A \underset{˙}{\cdot} X (x))$
41	32 40	eqtr4d	$⊢ φ \to (x \in I ⟼ A \cdot_{(I \times \{R\}) (x)} X (x)) = (I \times \{A\}) {\underset{˙}{\cdot}}_{f} X$
42	15 26 41	3eqtrd	$⊢ φ \to A \underset{˙}{∙} X = (I \times \{A\}) {\underset{˙}{\cdot}}_{f} X$

Metamath Proof Explorer

Theorem pwsvscafval

Proof