Theorem hgmapfval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

	Ref	Expression
Hypotheses	hgmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmapfval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmapfval.v	$$⊢V={\mathrm{Base}}_U$$
	hgmapfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hgmapfval.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmapfval.b	$$⊢B={\mathrm{Base}}_R$$
	hgmapfval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hgmapfval.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hgmapfval.m	$$⊢M=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hgmapfval.i	$$⊢I=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmapfval.k	$$⊢\phi \to \left(K\in Y\wedge W\in H\right)$$
Assertion	hgmapfval	$$⊢\phi \to I=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hgmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmapfval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmapfval.v	$$⊢V={\mathrm{Base}}_U$$
4		hgmapfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hgmapfval.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hgmapfval.b	$$⊢B={\mathrm{Base}}_R$$
7		hgmapfval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hgmapfval.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		hgmapfval.m	$$⊢M=\mathrm{HDMap}\left(K\right)\left(W\right)$$
10		hgmapfval.i	$$⊢I=\mathrm{HGMap}\left(K\right)\left(W\right)$$
11		hgmapfval.k	$$⊢\phi \to \left(K\in Y\wedge W\in H\right)$$
12	1	hgmapffval	$$⊢K\in Y\to \mathrm{HGMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$
13	12	fveq1d	$$⊢K\in Y\to \mathrm{HGMap}\left(K\right)\left(W\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\left(W\right)$$
14	10 13	syl5eq	$$⊢K\in Y\to I=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\left(W\right)$$
15		fveq2	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
16	15 2	eqtr4di	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=U$$
17		fveq2	$$⊢w=W\to \mathrm{HDMap}\left(K\right)\left(w\right)=\mathrm{HDMap}\left(K\right)\left(W\right)$$
18	17 9	eqtr4di	$$⊢w=W\to \mathrm{HDMap}\left(K\right)\left(w\right)=M$$
19		2fveq3	$$⊢w=W\to {\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}={\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
20	19	oveqd	$$⊢w=W\to y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)$$
21	20	eqeq2d	$$⊢w=W\to \left(m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\leftrightarrow m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)$$
22	21	ralbidv	$$⊢w=W\to \left(\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\leftrightarrow \forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)$$
23	22	riotabidv	$$⊢w=W\to \left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)=\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)$$
24	23	mpteq2dv	$$⊢w=W\to \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)=\left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)$$
25	24	eleq2d	$$⊢w=W\to \left(a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\right)$$
26	18 25	sbceqbid	$$⊢w=W\to \left(\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}M/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\right)$$
27	26	sbcbidv	$$⊢w=W\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}M/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\right)$$
28	16 27	sbceqbid	$$⊢w=W\to \left(\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}U/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}M/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\right)$$
29	2	fvexi	$$⊢U\in \mathrm{V}$$
30		fvex	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\in \mathrm{V}$$
31	9	fvexi	$$⊢M\in \mathrm{V}$$
32		simp2	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}$$
33		simp1	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to u=U$$
34	33	fveq2d	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to \mathrm{Scalar}\left(u\right)=\mathrm{Scalar}\left(U\right)$$
35	34 5	eqtr4di	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to \mathrm{Scalar}\left(u\right)=R$$
36	35	fveq2d	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}={\mathrm{Base}}_R$$
37	32 36	eqtrd	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to b={\mathrm{Base}}_R$$
38	37 6	eqtr4di	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to b=B$$
39		simp2	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to b=B$$
40		simp1	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to u=U$$
41	40	fveq2d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to {\mathrm{Base}}_u={\mathrm{Base}}_U$$
42	41 3	eqtr4di	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to {\mathrm{Base}}_u=V$$
43		simp3	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to m=M$$
44	40	fveq2d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to {\cdot }_u={\cdot }_U$$
45	44 4	eqtr4di	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to {\cdot }_u=\underset{\dot{}}{·}$$
46	45	oveqd	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to x{\cdot }_{u}v=x\underset{\dot{}}{·}v$$
47	43 46	fveq12d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to m\left(x{\cdot }_{u}v\right)=M\left(x\underset{\dot{}}{·}v\right)$$
48		eqidd	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
49	48 7	eqtr4di	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \mathrm{LCDual}\left(K\right)\left(W\right)=C$$
50	49	fveq2d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to {\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\cdot }_C$$
51	50 8	eqtr4di	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to {\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}=\underset{\dot{}}{\bullet }$$
52		eqidd	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to y=y$$
53	43	fveq1d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to m\left(v\right)=M\left(v\right)$$
54	51 52 53	oveq123d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)$$
55	47 54	eqeq12d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \left(m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\leftrightarrow M\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
56	42 55	raleqbidv	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \left(\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\leftrightarrow \forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
57	39 56	riotaeqbidv	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)=\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
58	39 57	mpteq12dv	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
59	58	eleq2d	$$⊢\left(u=U\wedge b=B\wedge m=M\right)\to \left(a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\leftrightarrow a\in \left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)\right)$$
60	38 59	syld3an2	$$⊢\left(u=U\wedge b={\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}\wedge m=M\right)\to \left(a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\leftrightarrow a\in \left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)\right)$$
61	29 30 31 60	sbc3ie	$$⊢\underset{\dot{}}{[}U/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}M/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(W\right)}m\left(v\right)\right)\right)\leftrightarrow a\in \left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
62	28 61	syl6bb	$$⊢w=W\to \left(\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow a\in \left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)\right)$$
63	62	abbi1dv	$$⊢w=W\to \left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
64		eqid	$$⊢\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$
65	63 64 6	mptfvmpt	$$⊢W\in H\to \left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\left(W\right)=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
66	14 65	sylan9eq	$$⊢\left(K\in Y\wedge W\in H\right)\to I=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
67	11 66	syl	$$⊢\phi \to I=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$