Metamath Proof Explorer

Theorem hlhilset

Description: The final Hilbert space constructed from a Hilbert lattice K and an arbitrary hyperplane W in K . (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hlhilset.l ⊢ 𝐿 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhilset.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hlhilset.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hlhilset.p ⊢ + = ( +g ‘ 𝑈 )
hlhilset.e ⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
hlhilset.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hlhilset.r ⊢ 𝑅 = ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , 𝐺 ⟩ )
hlhilset.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hlhilset.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hlhilset.i ⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) )
hlhilset.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion hlhilset ( 𝜑 → 𝐿 = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )

Proof

Step Hyp Ref Expression
1 hlhilset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhilset.l ⊢ 𝐿 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
3 hlhilset.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 hlhilset.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 hlhilset.p ⊢ + = ( +g ‘ 𝑈 )
6 hlhilset.e ⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
7 hlhilset.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
8 hlhilset.r ⊢ 𝑅 = ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , 𝐺 ⟩ )
9 hlhilset.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
10 hlhilset.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11 hlhilset.i ⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) )
12 hlhilset.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 elex ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ V )
14 13 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ V )
15 12 14 syl ⊢ ( 𝜑 → 𝐾 ∈ V )
16 1 fvexi ⊢ 𝐻 ∈ V
17 16 mptex ⊢ ( 𝑤 ∈ 𝐻 ↦ ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) ∈ V
18 nfcv ⊢ Ⅎ 𝑘 𝐾
19 nfcv ⊢ Ⅎ 𝑘 𝐻
20 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } )
21 19 20 nfmpt ⊢ Ⅎ 𝑘 ( 𝑤 ∈ 𝐻 ↦ ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) )
22 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
23 22 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
24 csbeq1a ⊢ ( 𝑘 = 𝐾 → ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) = ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) )
25 23 24 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) = ( 𝑤 ∈ 𝐻 ↦ ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
26 df-hlhil ⊢ HLHil = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
27 18 21 25 26 fvmptf ⊢ ( ( 𝐾 ∈ V ∧ ( 𝑤 ∈ 𝐻 ↦ ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) ∈ V ) → ( HLHil ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
28 15 17 27 sylancl ⊢ ( 𝜑 → ( HLHil ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
29 15 adantr ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → 𝐾 ∈ V )
30 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ∈ V )
31 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) → ( Base ‘ 𝑢 ) ∈ V )
32 id ⊢ ( 𝑣 = ( Base ‘ 𝑢 ) → 𝑣 = ( Base ‘ 𝑢 ) )
33 id ⊢ ( 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) → 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
35 34 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( DVecH ‘ 𝑘 ) = ( DVecH ‘ 𝐾 ) )
36 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → 𝑤 = 𝑊 )
37 35 36 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
38 37 3 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) = 𝑈 )
39 33 38 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) → 𝑢 = 𝑈 )
40 39 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) → ( Base ‘ 𝑢 ) = ( Base ‘ 𝑈 ) )
41 40 4 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) → ( Base ‘ 𝑢 ) = 𝑉 )
42 32 41 sylan9eqr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑣 = 𝑉 )
43 42 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ )
44 39 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑢 = 𝑈 )
45 44 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( +g ‘ 𝑢 ) = ( +g ‘ 𝑈 ) )
46 45 5 eqtr4di ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( +g ‘ 𝑢 ) = + )
47 46 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
48 34 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( EDRing ‘ 𝑘 ) = ( EDRing ‘ 𝐾 ) )
49 48 36 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
50 49 6 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) = 𝐸 )
51 34 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( HGMap ‘ 𝑘 ) = ( HGMap ‘ 𝐾 ) )
52 51 36 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) )
53 52 7 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) = 𝐺 )
54 53 opeq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ = ⟨ ( *𝑟 ‘ ndx ) , 𝐺 ⟩ )
55 50 54 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) = ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , 𝐺 ⟩ ) )
56 55 8 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) = 𝑅 )
57 56 opeq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ )
58 57 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ )
59 43 47 58 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } )
60 44 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( ·𝑠 ‘ 𝑢 ) = ( ·𝑠 ‘ 𝑈 ) )
61 60 9 eqtr4di ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( ·𝑠 ‘ 𝑢 ) = · )
62 61 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ )
63 34 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( HDMap ‘ 𝑘 ) = ( HDMap ‘ 𝐾 ) )
64 63 36 fveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) )
65 64 10 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) = 𝑆 )
66 65 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) = 𝑆 )
67 66 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
68 67 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) )
69 42 42 68 mpoeq123dv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑥 ) ) )
70 69 11 eqtr4di ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) = , )
71 70 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ = ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ )
72 62 71 preq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } = { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } )
73 59 72 uneq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
74 31 73 csbied ⊢ ( ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑢 = ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) → ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
75 30 74 csbied ⊢ ( ( ( 𝜑 ∧ 𝑤 = 𝑊 ) ∧ 𝑘 = 𝐾 ) → ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
76 29 75 csbied ⊢ ( ( 𝜑 ∧ 𝑤 = 𝑊 ) → ⦋ 𝐾 / 𝑘 ⦌ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
77 12 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
78 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∈ V
79 prex ⊢ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ∈ V
80 78 79 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∈ V
81 80 a1i ⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∈ V )
82 28 76 77 81 fvmptd ⊢ ( 𝜑 → ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 ) = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
83 2 82 eqtrid ⊢ ( 𝜑 → 𝐿 = ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )