Metamath Proof Explorer

Theorem 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 ∈ V ∧ I ∈ W → 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 ∈ V ∧ I ∈ W → Y = Scalar ⁡ R ⨉ 𝑠 I × R
5 4 fveq2d ⊢ R ∈ V ∧ I ∈ W → Base Y = Base Scalar ⁡ R ⨉ 𝑠 I × R
6 eqid ⊢ Scalar ⁡ R ⨉ 𝑠 I × R = Scalar ⁡ R ⨉ 𝑠 I × R
7 fvexd ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ R ∈ V
8 simpr ⊢ R ∈ V ∧ I ∈ W → I ∈ W
9 snex ⊢ R ∈ V
10 xpexg ⊢ I ∈ W ∧ R ∈ V → I × R ∈ V
11 8 9 10 sylancl ⊢ R ∈ V ∧ I ∈ W → I × R ∈ V
12 eqid ⊢ Base Scalar ⁡ R ⨉ 𝑠 I × R = Base Scalar ⁡ R ⨉ 𝑠 I × R
13 snnzg ⊢ R ∈ V → R ≠ ∅
14 13 adantr ⊢ R ∈ V ∧ I ∈ W → R ≠ ∅
15 dmxp ⊢ R ≠ ∅ → dom ⁡ I × R = I
16 14 15 syl ⊢ R ∈ V ∧ I ∈ W → dom ⁡ I × R = I
17 6 7 11 12 16 prdsbas ⊢ R ∈ V ∧ I ∈ W → Base Scalar ⁡ R ⨉ 𝑠 I × R = ⨉ x ∈ I Base I × R ⁡ x
18 fvconst2g ⊢ R ∈ V ∧ x ∈ I → I × R ⁡ x = R
19 18 fveq2d ⊢ R ∈ V ∧ x ∈ I → Base I × R ⁡ x = Base R
20 19 ralrimiva ⊢ R ∈ V → ∀ x ∈ I Base I × R ⁡ x = Base R
21 20 adantr ⊢ R ∈ V ∧ I ∈ W → ∀ x ∈ I Base I × R ⁡ x = Base R
22 ixpeq2 ⊢ ∀ x ∈ I Base I × R ⁡ x = Base R → ⨉ x ∈ I Base I × R ⁡ x = ⨉ x ∈ I Base R
23 21 22 syl ⊢ R ∈ V ∧ I ∈ W → ⨉ x ∈ I Base I × R ⁡ x = ⨉ x ∈ I Base R
24 17 23 eqtrd ⊢ R ∈ V ∧ I ∈ W → Base Scalar ⁡ R ⨉ 𝑠 I × R = ⨉ x ∈ I Base R
25 fvex ⊢ Base R ∈ V
26 ixpconstg ⊢ I ∈ W ∧ Base R ∈ V → ⨉ x ∈ I Base R = Base R I
27 8 25 26 sylancl ⊢ R ∈ V ∧ I ∈ W → ⨉ x ∈ I Base R = Base R I
28 2 oveq1i ⊢ B I = Base R I
29 27 28 eqtr4di ⊢ R ∈ V ∧ I ∈ W → ⨉ x ∈ I Base R = B I
30 5 24 29 3eqtrrd ⊢ R ∈ V ∧ I ∈ W → B I = Base Y