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 → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )