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 β†’ 𝑁 = ( π‘₯ ∈ 𝑉 ↦ ( √ β€˜ ( π‘₯ , π‘₯ ) ) ) )