pwsbas

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

	Ref	Expression
Hypotheses	pwsbas.y	$⊢ Y = R ↑_{𝑠} I$
	pwsbas.f	$⊢ B = {Base}_{R}$
Assertion	pwsbas	$⊢ (R \in V \land I \in W) \to B^{I} = {Base}_{Y}$

Proof

Step	Hyp	Ref	Expression
1		pwsbas.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsbas.f	$⊢ B = {Base}_{R}$
3		eqid	$⊢ Scalar (R) = Scalar (R)$
4	1 3	pwsval	$⊢ (R \in V \land I \in W) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
5	4	fveq2d	$⊢ (R \in V \land I \in W) \to {Base}_{Y} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
6		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
7		fvexd	$⊢ (R \in V \land I \in W) \to Scalar (R) \in V$
8		simpr	$⊢ (R \in V \land I \in W) \to I \in W$
9		snex	$⊢ \{R\} \in V$
10		xpexg	$⊢ (I \in W \land \{R\} \in V) \to I \times \{R\} \in V$
11	8 9 10	sylancl	$⊢ (R \in V \land I \in W) \to I \times \{R\} \in V$
12		eqid	$⊢ {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
13		snnzg	$⊢ R \in V \to \{R\} \neq \emptyset$
14	13	adantr	$⊢ (R \in V \land I \in W) \to \{R\} \neq \emptyset$
15		dmxp	$⊢ \{R\} \neq \emptyset \to dom (I \times \{R\}) = I$
16	14 15	syl	$⊢ (R \in V \land I \in W) \to dom (I \times \{R\}) = I$
17	6 7 11 12 16	prdsbas	$⊢ (R \in V \land I \in W) \to {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = \underset{x \in I}{⨉} {Base}_{(I \times \{R\}) (x)}$
18		fvconst2g	$⊢ (R \in V \land x \in I) \to (I \times \{R\}) (x) = R$
19	18	fveq2d	$⊢ (R \in V \land x \in I) \to {Base}_{(I \times \{R\}) (x)} = {Base}_{R}$
20	19	ralrimiva	$⊢ R \in V \to \forall x \in I {Base}_{(I \times \{R\}) (x)} = {Base}_{R}$
21	20	adantr	$⊢ (R \in V \land I \in W) \to \forall x \in I {Base}_{(I \times \{R\}) (x)} = {Base}_{R}$
22		ixpeq2	$⊢ \forall x \in I {Base}_{(I \times \{R\}) (x)} = {Base}_{R} \to \underset{x \in I}{⨉} {Base}_{(I \times \{R\}) (x)} = \underset{x \in I}{⨉} {Base}_{R}$
23	21 22	syl	$⊢ (R \in V \land I \in W) \to \underset{x \in I}{⨉} {Base}_{(I \times \{R\}) (x)} = \underset{x \in I}{⨉} {Base}_{R}$
24	17 23	eqtrd	$⊢ (R \in V \land I \in W) \to {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = \underset{x \in I}{⨉} {Base}_{R}$
25		fvex	$⊢ {Base}_{R} \in V$
26		ixpconstg	$⊢ (I \in W \land {Base}_{R} \in V) \to \underset{x \in I}{⨉} {Base}_{R} = {Base}_{R}^{I}$
27	8 25 26	sylancl	$⊢ (R \in V \land I \in W) \to \underset{x \in I}{⨉} {Base}_{R} = {Base}_{R}^{I}$
28	2	oveq1i	$⊢ B^{I} = {Base}_{R}^{I}$
29	27 28	eqtr4di	$⊢ (R \in V \land I \in W) \to \underset{x \in I}{⨉} {Base}_{R} = B^{I}$
30	5 24 29	3eqtrrd	$⊢ (R \in V \land I \in W) \to B^{I} = {Base}_{Y}$

Metamath Proof Explorer

Theorem pwsbas

Proof