This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcphval

Description: Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
tcphval.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
Assertion tcphval 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 tcphval.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
4 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
5 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
6 5 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
7 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑖 ‘ 𝑤 ) = ( ·𝑖 ‘ 𝑊 ) )
8 7 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑖 ‘ 𝑤 ) = , )
9 8 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) = ( 𝑥 , 𝑥 ) )
10 9 fveq2d ⊢ ( 𝑤 = 𝑊 → ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) = ( √ ‘ ( 𝑥 , 𝑥 ) ) )
11 6 10 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
12 4 11 oveq12d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )
13 df-tcph ⊢ toℂPreHil = ( 𝑤 ∈ V ↦ ( 𝑤 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) )
14 ovex ⊢ ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ∈ V
15 12 13 14 fvmpt ⊢ ( 𝑊 ∈ V → ( toℂPreHil ‘ 𝑊 ) = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )
16 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( toℂPreHil ‘ 𝑊 ) = ∅ )
17 reldmtng ⊢ Rel dom toNrmGrp
18 17 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) = ∅ )
19 16 18 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( toℂPreHil ‘ 𝑊 ) = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )
20 15 19 pm2.61i ⊢ ( toℂPreHil ‘ 𝑊 ) = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
21 1 20 eqtri ⊢ 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )