Metamath Proof Explorer


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 = LHyp K
hgmapvv.u U = DVecH K W
hgmapvv.r R = Scalar U
hgmapvv.b B = Base R
hgmapvv.g G = HGMap K W
hgmapvv.k φ K HL W H
hgmapvv.j φ X B
Assertion hgmapvv φ G G X = X

Proof

Step Hyp Ref Expression
1 hgmapvv.h H = LHyp K
2 hgmapvv.u U = DVecH K W
3 hgmapvv.r R = Scalar U
4 hgmapvv.b B = Base R
5 hgmapvv.g G = HGMap K W
6 hgmapvv.k φ K HL W H
7 hgmapvv.j φ X B
8 2fveq3 X = 0 R G G X = G G 0 R
9 id X = 0 R X = 0 R
10 8 9 eqeq12d X = 0 R G G X = X G G 0 R = 0 R
11 eqid I Base K I LTrn K W = I Base K I LTrn K W
12 eqid ocH K W = ocH K W
13 eqid Base U = Base U
14 eqid U = U
15 eqid R = R
16 eqid 0 R = 0 R
17 eqid 1 R = 1 R
18 eqid inv r R = inv r R
19 eqid HDMap K W = HDMap K W
20 6 adantr φ X 0 R K HL W H
21 7 anim1i φ X 0 R X B X 0 R
22 eldifsn X B 0 R X B X 0 R
23 21 22 sylibr φ X 0 R X B 0 R
24 1 11 12 2 13 14 3 4 15 16 17 18 19 5 20 23 hgmapvvlem3 φ X 0 R G G X = X
25 1 2 3 16 5 6 hgmapval0 φ G 0 R = 0 R
26 25 fveq2d φ G G 0 R = G 0 R
27 26 25 eqtrd φ G G 0 R = 0 R
28 10 24 27 pm2.61ne φ G G X = X