Metamath Proof Explorer

Theorem resspwsds

Description: Restriction of a power metric. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses resspwsds.y ⊢ ( 𝜑 → 𝑌 = ( 𝑅 ↑s 𝐼 ) )
resspwsds.h ⊢ ( 𝜑 → 𝐻 = ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 ) )
resspwsds.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
resspwsds.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
resspwsds.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
resspwsds.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
resspwsds.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
resspwsds.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion resspwsds ( 𝜑 → 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 resspwsds.y ⊢ ( 𝜑 → 𝑌 = ( 𝑅 ↑s 𝐼 ) )
2 resspwsds.h ⊢ ( 𝜑 → 𝐻 = ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 ) )
3 resspwsds.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
4 resspwsds.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
5 resspwsds.e ⊢ 𝐸 = ( dist ‘ 𝐻 )
6 resspwsds.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 resspwsds.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
8 resspwsds.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
9 eqid ⊢ ( 𝑅 ↑s 𝐼 ) = ( 𝑅 ↑s 𝐼 )
10 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
11 9 10 pwsval ⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉 ) → ( 𝑅 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
12 7 6 11 syl2anc ⊢ ( 𝜑 → ( 𝑅 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
13 fconstmpt ⊢ ( 𝐼 × { 𝑅 } ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
14 13 oveq2i ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
15 12 14 eqtrdi ⊢ ( 𝜑 → ( 𝑅 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) )
16 1 15 eqtrd ⊢ ( 𝜑 → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ) )
17 ovex ⊢ ( 𝑅 ↾s 𝐴 ) ∈ V
18 eqid ⊢ ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 ) = ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 )
19 eqid ⊢ ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) )
20 18 19 pwsval ⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) Xs ( 𝐼 × { ( 𝑅 ↾s 𝐴 ) } ) ) )
21 17 6 20 sylancr ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) Xs ( 𝐼 × { ( 𝑅 ↾s 𝐴 ) } ) ) )
22 fconstmpt ⊢ ( 𝐼 × { ( 𝑅 ↾s 𝐴 ) } ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) )
23 22 oveq2i ⊢ ( ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) Xs ( 𝐼 × { ( 𝑅 ↾s 𝐴 ) } ) ) = ( ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) )
24 21 23 eqtrdi ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝐴 ) ↑s 𝐼 ) = ( ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) )
25 2 24 eqtrd ⊢ ( 𝜑 → 𝐻 = ( ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ↾s 𝐴 ) ) ) )
26 fvexd ⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
27 fvexd ⊢ ( 𝜑 → ( Scalar ‘ ( 𝑅 ↾s 𝐴 ) ) ∈ V )
28 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑊 )
29 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ 𝑋 )
30 16 25 3 4 5 26 27 6 28 29 ressprdsds ⊢ ( 𝜑 → 𝐸 = ( 𝐷 ↾ ( 𝐵 × 𝐵 ) ) )