Theorem hlhilip

Description: 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.p	⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) )
Assertion	hlhilip	⊢ ( 𝜑 → , = ( ·𝑖 ‘ 𝑈 ) )

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.p	⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) )
8	3	fvexi	⊢ 𝑉 ∈ V
9	8 8	mpoex	⊢ ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) ∈ V
10	7 9	eqeltri	⊢ , ∈ V
11		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝐿 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝐿 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } )
12	11	phlip	⊢ ( , ∈ V → , = ( ·𝑖 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝐿 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ) )
13	10 12	ax-mp	⊢ , = ( ·𝑖 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝐿 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
14		eqid	⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
15		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
16		eqid	⊢ ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
17		eqid	⊢ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) = ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ )
18		eqid	⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
19	1 5 2 3 14 15 16 17 18 4 7 6	hlhilset	⊢ ( 𝜑 → 𝑈 = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝐿 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
20	19	fveq2d	⊢ ( 𝜑 → ( ·𝑖 ‘ 𝑈 ) = ( ·𝑖 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝐿 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ) )
21	13 20	eqtr4id	⊢ ( 𝜑 → , = ( ·𝑖 ‘ 𝑈 ) )