Metamath Proof Explorer

Theorem pwsbas

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

Ref Expression
Hypotheses pwsbas.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsbas.f ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion pwsbas ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐵 ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pwsbas.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsbas.f ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
4 1 3 pwsval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
5 4 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
6 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
7 fvexd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑅 ) ∈ V )
8 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ∈ 𝑊 )
9 snex ⊢ { 𝑅 } ∈ V
10 xpexg ⊢ ( ( 𝐼 ∈ 𝑊 ∧ { 𝑅 } ∈ V ) → ( 𝐼 × { 𝑅 } ) ∈ V )
11 8 9 10 sylancl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑅 } ) ∈ V )
12 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
13 snnzg ⊢ ( 𝑅 ∈ 𝑉 → { 𝑅 } ≠ ∅ )
14 13 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑅 } ≠ ∅ )
15 dmxp ⊢ ( { 𝑅 } ≠ ∅ → dom ( 𝐼 × { 𝑅 } ) = 𝐼 )
16 14 15 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → dom ( 𝐼 × { 𝑅 } ) = 𝐼 )
17 6 7 11 12 16 prdsbas ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) )
18 fvconst2g ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
19 18 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( Base ‘ 𝑅 ) )
20 19 ralrimiva ⊢ ( 𝑅 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( Base ‘ 𝑅 ) )
21 20 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( Base ‘ 𝑅 ) )
22 ixpeq2 ⊢ ( ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( Base ‘ 𝑅 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) )
23 21 22 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) )
24 17 23 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) )
25 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
26 ixpconstg ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( Base ‘ 𝑅 ) ∈ V ) → X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
27 8 25 26 sylancl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
28 2 oveq1i ⊢ ( 𝐵 ↑m 𝐼 ) = ( ( Base ‘ 𝑅 ) ↑m 𝐼 )
29 27 28 eqtr4di ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → X 𝑥 ∈ 𝐼 ( Base ‘ 𝑅 ) = ( 𝐵 ↑m 𝐼 ) )
30 5 24 29 3eqtrrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐵 ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )