Theorem hdmapval

Description: Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in Baer p. 48. We select a convenient fixed reference vector E to be <. 0 , 1 >. (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom P = ( ( ocK )W ) (see dvheveccl ). ( JE ) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our z that the A. z e. V ranges over. The middle term ( I<. E , ( JE ) , z >. ) provides isolation to allow E and T to assume the same value without conflict. Closure is shown by hdmapcl . If a separate auxiliary vector is known, hdmapval2 provides a version without quantification. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapfval.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapfval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapfval.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapfval.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmapfval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmapfval.d	$$⊢D={\mathrm{Base}}_C$$
	hdmapfval.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hdmapfval.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmapfval.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapfval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
	hdmapval.t	$$⊢\phi \to T\in V$$
Assertion	hdmapval	$$⊢\phi \to S\left(T\right)=\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapfval.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapfval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		hdmapfval.v	$$⊢V={\mathrm{Base}}_U$$
5		hdmapfval.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
6		hdmapfval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		hdmapfval.d	$$⊢D={\mathrm{Base}}_C$$
8		hdmapfval.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
9		hdmapfval.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
10		hdmapfval.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
11		hdmapfval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
12		hdmapval.t	$$⊢\phi \to T\in V$$
13	1 2 3 4 5 6 7 8 9 10 11	hdmapfval	$$⊢\phi \to S=\left(t\in V⟼\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)\right)$$
14	13	fveq1d	$$⊢\phi \to S\left(T\right)=\left(t\in V⟼\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)\right)\left(T\right)$$
15		riotaex	$$⊢\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)\in \mathrm{V}$$
16		sneq	$$⊢t=T\to \left\{t\right\}=\left\{T\right\}$$
17	16	fveq2d	$$⊢t=T\to N\left(\left\{t\right\}\right)=N\left(\left\{T\right\}\right)$$
18	17	uneq2d	$$⊢t=T\to N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)=N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)$$
19	18	eleq2d	$$⊢t=T\to \left(z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\leftrightarrow z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\right)$$
20	19	notbid	$$⊢t=T\to \left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\leftrightarrow \neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\right)$$
21		oteq3	$$⊢t=T\to ⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩=⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩$$
22	21	fveq2d	$$⊢t=T\to I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)$$
23	22	eqeq2d	$$⊢t=T\to \left(y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\leftrightarrow y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)$$
24	20 23	imbi12d	$$⊢t=T\to \left(\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\leftrightarrow \left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$
25	24	ralbidv	$$⊢t=T\to \left(\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\leftrightarrow \forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$
26	25	riotabidv	$$⊢t=T\to \left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)=\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$
27		eqid	$$⊢\left(t\in V⟼\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)\right)=\left(t\in V⟼\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)\right)$$
28	26 27	fvmptg	$$⊢\left(T\in V\wedge \left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)\in \mathrm{V}\right)\to \left(t\in V⟼\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)\right)\left(T\right)=\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$
29	12 15 28	sylancl	$$⊢\phi \to \left(t\in V⟼\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{t\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),t⟩\right)\right)\right)\right)\left(T\right)=\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$
30	14 29	eqtrd	$$⊢\phi \to S\left(T\right)=\left(\iota y\in D|\forall z\in V\left(\neg z\in \left(N\left(\left\{E\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨E,J\left(E\right),z⟩\right),T⟩\right)\right)\right)$$