pwsval

Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Step	Hyp	Ref	Expression
1		pwsval.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsval.f	$⊢ F = Scalar (R)$
3		elex	$⊢ R \in V \to R \in V$
4		elex	$⊢ I \in W \to I \in V$
5		simpl	$⊢ (r = R \land i = I) \to r = R$
6	5	fveq2d	$⊢ (r = R \land i = I) \to Scalar (r) = Scalar (R)$
7	6 2	eqtr4di	$⊢ (r = R \land i = I) \to Scalar (r) = F$
8		id	$⊢ i = I \to i = I$
9		sneq	$⊢ r = R \to \{r\} = \{R\}$
10		xpeq12	$⊢ (i = I \land \{r\} = \{R\}) \to i \times \{r\} = I \times \{R\}$
11	8 9 10	syl2anr	$⊢ (r = R \land i = I) \to i \times \{r\} = I \times \{R\}$
12	7 11	oveq12d	$⊢ (r = R \land i = I) \to Scalar (r) ⨉_{𝑠} (i \times \{r\}) = F ⨉_{𝑠} (I \times \{R\})$
13		df-pws	$⊢ ↑_{𝑠} = (r \in V, i \in V ⟼ Scalar (r) ⨉_{𝑠} (i \times \{r\}))$
14		ovex	$⊢ F ⨉_{𝑠} (I \times \{R\}) \in V$
15	12 13 14	ovmpoa	$⊢ (R \in V \land I \in V) \to R ↑_{𝑠} I = F ⨉_{𝑠} (I \times \{R\})$
16	3 4 15	syl2an	$⊢ (R \in V \land I \in W) \to R ↑_{𝑠} I = F ⨉_{𝑠} (I \times \{R\})$
17	1 16	eqtrid	$⊢ (R \in V \land I \in W) \to Y = F ⨉_{𝑠} (I \times \{R\})$

Metamath Proof Explorer