pwssca

Description: The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

Step	Hyp	Ref	Expression
1		pwssca.y	$⊢ Y = R ↑_{𝑠} I$
2		pwssca.s	$⊢ S = Scalar (R)$
3		eqid	$⊢ S ⨉_{𝑠} (I \times \{R\}) = S ⨉_{𝑠} (I \times \{R\})$
4	2	fvexi	$⊢ S \in V$
5	4	a1i	$⊢ (R \in V \land I \in W) \to S \in V$
6		simpr	$⊢ (R \in V \land I \in W) \to I \in W$
7		snex	$⊢ \{R\} \in V$
8		xpexg	$⊢ (I \in W \land \{R\} \in V) \to I \times \{R\} \in V$
9	6 7 8	sylancl	$⊢ (R \in V \land I \in W) \to I \times \{R\} \in V$
10	3 5 9	prdssca	$⊢ (R \in V \land I \in W) \to S = Scalar (S ⨉_{𝑠} (I \times \{R\}))$
11	1 2	pwsval	$⊢ (R \in V \land I \in W) \to Y = S ⨉_{𝑠} (I \times \{R\})$
12	11	fveq2d	$⊢ (R \in V \land I \in W) \to Scalar (Y) = Scalar (S ⨉_{𝑠} (I \times \{R\}))$
13	10 12	eqtr4d	$⊢ (R \in V \land I \in W) \to S = Scalar (Y)$

Metamath Proof Explorer