Theorem hlhilipval

Description: Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilip.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hlhilip.l	⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hlhilip.v	⊢ 𝑉 = ( Base ‘ 𝐿 )
	hlhilip.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hlhilip.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
	hlhilip.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hlhilip.i	⊢ , = ( ·𝑖 ‘ 𝑈 )
	hlhilip.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hlhilip.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	hlhilipval	⊢ ( 𝜑 → ( 𝑋 , 𝑌 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilip.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hlhilip.l	⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hlhilip.v	⊢ 𝑉 = ( Base ‘ 𝐿 )
4		hlhilip.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5		hlhilip.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
6		hlhilip.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		hlhilip.i	⊢ , = ( ·𝑖 ‘ 𝑈 )
8		hlhilip.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		hlhilip.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10		eqid	⊢ ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) )
11	1 2 3 4 5 6 10	hlhilip	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( ·𝑖 ‘ 𝑈 ) )
12	7 11	eqtr4id	⊢ ( 𝜑 → , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) )
13	12	oveqd	⊢ ( 𝜑 → ( 𝑋 , 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑌 ) )
14		fveq2	⊢ ( 𝑥 = 𝑋 → ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑋 ) )
15		fveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑌 ) )
16	15	fveq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) )
17		fvex	⊢ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ∈ V
18	14 16 10 17	ovmpo	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑌 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) )
19	8 9 18	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑌 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) )
20	13 19	eqtrd	⊢ ( 𝜑 → ( 𝑋 , 𝑌 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) )