Theorem hgmapvv

Description: Value of a double involution. Part 1.2 of Baer p. 110 line 37. (Contributed by NM, 13-Jun-2015)

	Ref	Expression
Hypotheses	hgmapvv.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmapvv.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmapvv.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmapvv.b	$$⊢B={\mathrm{Base}}_R$$
	hgmapvv.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmapvv.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hgmapvv.j	$$⊢\phi \to X\in B$$
Assertion	hgmapvv	$$⊢\phi \to G\left(G\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		hgmapvv.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmapvv.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmapvv.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		hgmapvv.b	$$⊢B={\mathrm{Base}}_R$$
5		hgmapvv.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
6		hgmapvv.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		hgmapvv.j	$$⊢\phi \to X\in B$$
8		2fveq3	$$⊢X=0_R\to G\left(G\left(X\right)\right)=G\left(G\left(0_R\right)\right)$$
9		id	$$⊢X=0_R\to X=0_R$$
10	8 9	eqeq12d	$$⊢X=0_R\to \left(G\left(G\left(X\right)\right)=X\leftrightarrow G\left(G\left(0_R\right)\right)=0_R\right)$$
11		eqid	$$⊢⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
12		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
13		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
14		eqid	$$⊢{\cdot }_U={\cdot }_U$$
15		eqid	$$⊢{\cdot }_R={\cdot }_R$$
16		eqid	$$⊢0_R=0_R$$
17		eqid	$$⊢1_R=1_R$$
18		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
19		eqid	$$⊢\mathrm{HDMap}\left(K\right)\left(W\right)=\mathrm{HDMap}\left(K\right)\left(W\right)$$
20	6	adantr	$$⊢\left(\phi \wedge X\ne 0_R\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
21	7	anim1i	$$⊢\left(\phi \wedge X\ne 0_R\right)\to \left(X\in B\wedge X\ne 0_R\right)$$
22		eldifsn	$$⊢X\in \left(B\setminus \left\{0_R\right\}\right)\leftrightarrow \left(X\in B\wedge X\ne 0_R\right)$$
23	21 22	sylibr	$$⊢\left(\phi \wedge X\ne 0_R\right)\to X\in \left(B\setminus \left\{0_R\right\}\right)$$
24	1 11 12 2 13 14 3 4 15 16 17 18 19 5 20 23	hgmapvvlem3	$$⊢\left(\phi \wedge X\ne 0_R\right)\to G\left(G\left(X\right)\right)=X$$
25	1 2 3 16 5 6	hgmapval0	$$⊢\phi \to G\left(0_R\right)=0_R$$
26	25	fveq2d	$$⊢\phi \to G\left(G\left(0_R\right)\right)=G\left(0_R\right)$$
27	26 25	eqtrd	$$⊢\phi \to G\left(G\left(0_R\right)\right)=0_R$$
28	10 24 27	pm2.61ne	$$⊢\phi \to G\left(G\left(X\right)\right)=X$$