# Metamath Proof Explorer

## Theorem hgmapvvlem1

Description: Involution property of scalar sigma map. Line 10 in Baer p. 111, t sigma squared = t. Our E , C , D , Y , X correspond to Baer's w, h, k, s, t. (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hdmapglem6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapglem6.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
hdmapglem6.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hdmapglem6.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapglem6.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapglem6.q
hdmapglem6.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hdmapglem6.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
hdmapglem6.t
hdmapglem6.z
hdmapglem6.i
hdmapglem6.n ${⊢}{N}={inv}_{r}\left({R}\right)$
hdmapglem6.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapglem6.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
hdmapglem6.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmapglem6.x
hdmapglem6.c ${⊢}{\phi }\to {C}\in {O}\left(\left\{{E}\right\}\right)$
hdmapglem6.d ${⊢}{\phi }\to {D}\in {O}\left(\left\{{E}\right\}\right)$
hdmapglem6.cd
hdmapglem6.y
hdmapglem6.yx
Assertion hgmapvvlem1 ${⊢}{\phi }\to {G}\left({G}\left({X}\right)\right)={X}$

### Proof

Step Hyp Ref Expression
1 hdmapglem6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapglem6.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
3 hdmapglem6.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
4 hdmapglem6.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 hdmapglem6.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 hdmapglem6.q
7 hdmapglem6.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
8 hdmapglem6.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
9 hdmapglem6.t
10 hdmapglem6.z
11 hdmapglem6.i
12 hdmapglem6.n ${⊢}{N}={inv}_{r}\left({R}\right)$
13 hdmapglem6.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
14 hdmapglem6.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
15 hdmapglem6.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
16 hdmapglem6.x
17 hdmapglem6.c ${⊢}{\phi }\to {C}\in {O}\left(\left\{{E}\right\}\right)$
18 hdmapglem6.d ${⊢}{\phi }\to {D}\in {O}\left(\left\{{E}\right\}\right)$
19 hdmapglem6.cd
20 hdmapglem6.y
21 hdmapglem6.yx
22 1 4 15 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
23 7 lmodring ${⊢}{U}\in \mathrm{LMod}\to {R}\in \mathrm{Ring}$
24 22 23 syl ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
25 16 eldifad ${⊢}{\phi }\to {X}\in {B}$
26 1 4 7 8 14 15 25 hgmapcl ${⊢}{\phi }\to {G}\left({X}\right)\in {B}$
27 1 4 7 8 14 15 26 hgmapcl ${⊢}{\phi }\to {G}\left({G}\left({X}\right)\right)\in {B}$
28 20 eldifad ${⊢}{\phi }\to {Y}\in {B}$
29 1 4 7 8 14 15 28 hgmapcl ${⊢}{\phi }\to {G}\left({Y}\right)\in {B}$
30 1 4 15 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
31 7 lvecdrng ${⊢}{U}\in \mathrm{LVec}\to {R}\in \mathrm{DivRing}$
32 30 31 syl ${⊢}{\phi }\to {R}\in \mathrm{DivRing}$
33 eldifsni
34 20 33 syl
35 1 4 7 8 10 14 15 28 hgmapeq0
36 35 necon3bid
37 34 36 mpbird
38 8 10 12 drnginvrcl
39 32 29 37 38 syl3anc ${⊢}{\phi }\to {N}\left({G}\left({Y}\right)\right)\in {B}$
40 8 9 ringass
41 24 27 29 39 40 syl13anc
42 8 10 9 11 12 drnginvrr
43 32 29 37 42 syl3anc
44 43 oveq2d
45 8 9 11 ringridm
46 24 27 45 syl2anc
47 41 44 46 3eqtrrd
48 21 fveq2d
49 1 4 7 8 9 14 15 28 26 hgmapmul
50 48 49 eqtr3d
51 19 fveq2d
52 eqid ${⊢}{+}_{{U}}={+}_{{U}}$
53 eqid ${⊢}{-}_{{U}}={-}_{{U}}$
54 1 2 3 4 5 52 53 6 7 8 9 10 13 14 15 17 18 28 25 hdmapglem5 ${⊢}{\phi }\to {G}\left({S}\left({D}\right)\left({C}\right)\right)={S}\left({C}\right)\left({D}\right)$
55 51 54 eqtr3d
56 50 55 eqtr3d
57 21 19 eqtr4d
58 1 2 3 4 5 52 53 6 7 8 9 10 13 14 15 17 18 28 25 57 hdmapinvlem4
59 56 58 eqtr4d
60 59 oveq1d
61 8 9 ringass
62 24 25 29 39 61 syl13anc
63 43 oveq2d
64 8 9 11 ringridm
65 24 25 64 syl2anc
66 62 63 65 3eqtrd
67 47 60 66 3eqtrd ${⊢}{\phi }\to {G}\left({G}\left({X}\right)\right)={X}$