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