Theorem lcdneg

Description: The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	lcdneg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdneg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdneg.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	lcdneg.m	$$⊢M={inv}_g\left(R\right)$$
	lcdneg.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdneg.s	$$⊢S=\mathrm{Scalar}\left(C\right)$$
	lcdneg.n	$$⊢N={inv}_g\left(S\right)$$
	lcdneg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcdneg	$$⊢\phi \to N=M$$

Proof

Step	Hyp	Ref	Expression
1		lcdneg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdneg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdneg.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		lcdneg.m	$$⊢M={inv}_g\left(R\right)$$
5		lcdneg.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcdneg.s	$$⊢S=\mathrm{Scalar}\left(C\right)$$
7		lcdneg.n	$$⊢N={inv}_g\left(S\right)$$
8		lcdneg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
10	1 2 3 9 5 6 8	lcdsca	$$⊢\phi \to S={opp}_r\left(R\right)$$
11	10	fveq2d	$$⊢\phi \to {inv}_g\left(S\right)={inv}_g\left({opp}_r\left(R\right)\right)$$
12	9 4	opprneg	$$⊢M={inv}_g\left({opp}_r\left(R\right)\right)$$
13	11 7 12	3eqtr4g	$$⊢\phi \to N=M$$