Theorem hlhilvsca

Description: The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilvsca.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hlhilvsca.l	⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hlhilvsca.t	⊢ · = ( ·𝑠 ‘ 𝐿 )
	hlhilvsca.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
	hlhilvsca.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hlhilvsca	⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilvsca.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hlhilvsca.l	⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hlhilvsca.t	⊢ · = ( ·𝑠 ‘ 𝐿 )
4		hlhilvsca.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
5		hlhilvsca.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6	3	fvexi	⊢ · ∈ V
7		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝐿 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝐿 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } )
8	7	phlvsca	⊢ ( · ∈ V → · = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝐿 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
9	6 8	ax-mp	⊢ · = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝐿 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) )
10		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
11		eqid	⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
12		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
13		eqid	⊢ ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
14		eqid	⊢ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) = ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ )
15		eqid	⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
16		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) )
17	1 4 2 10 11 12 13 14 3 15 16 5	hlhilset	⊢ ( 𝜑 → 𝑈 = ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝐿 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) )
18	17	fveq2d	⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝐿 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝐿 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝐿 ) , 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
19	9 18	eqtr4id	⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑈 ) )