Metamath Proof Explorer

Theorem hlhilsca

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

Ref Expression
Hypotheses hlhilbase.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hlhilbase.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhilbase.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hlhilsca.e ⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
hlhilsca.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hlhilsca.r ⊢ 𝑅 = ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , 𝐺 ⟩ )
Assertion hlhilsca ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑈 ) )

Proof

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