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 ) , , ⟩ } ) )