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

Metamath Proof Explorer

Theorem tchnmfval

Description: The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphnmval.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 tcphnmval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 tcphnmval.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
5 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) )
6 fvrn0 ⊢ ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ ( ran √ ∪ { ∅ } )
7 6 a1i ⊢ ( 𝑥 ∈ 𝑉 → ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ ( ran √ ∪ { ∅ } ) )
8 5 7 fmpti ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) : 𝑉 ⟶ ( ran √ ∪ { ∅ } )
9 1 3 4 tcphval ⊢ 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
10 cnex ⊢ ℂ ∈ V
11 sqrtf ⊢ √ : ℂ ⟶ ℂ
12 frn ⊢ ( √ : ℂ ⟶ ℂ → ran √ ⊆ ℂ )
13 11 12 ax-mp ⊢ ran √ ⊆ ℂ
14 10 13 ssexi ⊢ ran √ ∈ V
15 p0ex ⊢ { ∅ } ∈ V
16 14 15 unex ⊢ ( ran √ ∪ { ∅ } ) ∈ V
17 9 3 16 tngnm ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) : 𝑉 ⟶ ( ran √ ∪ { ∅ } ) ) → ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) = ( norm ‘ 𝐺 ) )
18 8 17 mpan2 ⊢ ( 𝑊 ∈ Grp → ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) = ( norm ‘ 𝐺 ) )
19 2 18 eqtr4id ⊢ ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )