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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmapglem6.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapglem6.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapglem6.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	hdmapglem6.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapglem6.i	$$⊢\underset{\dot{}}{1}=1_R$$
	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	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	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	$$⊢\phi \to S\left(D\right)\left(C\right)=\underset{\dot{}}{1}$$
	hdmapglem6.y	$$⊢\phi \to Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmapglem6.yx	$$⊢\phi \to Y\underset{\dot{}}{\times }G\left(X\right)=\underset{\dot{}}{1}$$
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}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\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	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		hdmapglem6.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
8		hdmapglem6.b	$$⊢B={\mathrm{Base}}_R$$
9		hdmapglem6.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
10		hdmapglem6.z	$$⊢\underset{\dot{}}{0}=0_R$$
11		hdmapglem6.i	$$⊢\underset{\dot{}}{1}=1_R$$
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	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
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	$$⊢\phi \to S\left(D\right)\left(C\right)=\underset{\dot{}}{1}$$
20		hdmapglem6.y	$$⊢\phi \to Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
21		hdmapglem6.yx	$$⊢\phi \to Y\underset{\dot{}}{\times }G\left(X\right)=\underset{\dot{}}{1}$$
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	$$⊢Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to Y\ne \underset{\dot{}}{0}$$
34	20 33	syl	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
35	1 4 7 8 10 14 15 28	hgmapeq0	$$⊢\phi \to \left(G\left(Y\right)=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
36	35	necon3bid	$$⊢\phi \to \left(G\left(Y\right)\ne \underset{\dot{}}{0}\leftrightarrow Y\ne \underset{\dot{}}{0}\right)$$
37	34 36	mpbird	$$⊢\phi \to G\left(Y\right)\ne \underset{\dot{}}{0}$$
38	8 10 12	drnginvrcl	$$⊢\left(R\in \mathrm{DivRing}\wedge G\left(Y\right)\in B\wedge G\left(Y\right)\ne \underset{\dot{}}{0}\right)\to N\left(G\left(Y\right)\right)\in B$$
39	32 29 37 38	syl3anc	$$⊢\phi \to N\left(G\left(Y\right)\right)\in B$$
40	8 9	ringass	$$⊢\left(R\in \mathrm{Ring}\wedge \left(G\left(G\left(X\right)\right)\in B\wedge G\left(Y\right)\in B\wedge N\left(G\left(Y\right)\right)\in B\right)\right)\to \left(G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=G\left(G\left(X\right)\right)\underset{\dot{}}{\times }\left(G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)\right)$$
41	24 27 29 39 40	syl13anc	$$⊢\phi \to \left(G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=G\left(G\left(X\right)\right)\underset{\dot{}}{\times }\left(G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)\right)$$
42	8 10 9 11 12	drnginvrr	$$⊢\left(R\in \mathrm{DivRing}\wedge G\left(Y\right)\in B\wedge G\left(Y\right)\ne \underset{\dot{}}{0}\right)\to G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=\underset{\dot{}}{1}$$
43	32 29 37 42	syl3anc	$$⊢\phi \to G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=\underset{\dot{}}{1}$$
44	43	oveq2d	$$⊢\phi \to G\left(G\left(X\right)\right)\underset{\dot{}}{\times }\left(G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)\right)=G\left(G\left(X\right)\right)\underset{\dot{}}{\times }\underset{\dot{}}{1}$$
45	8 9 11	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge G\left(G\left(X\right)\right)\in B\right)\to G\left(G\left(X\right)\right)\underset{\dot{}}{\times }\underset{\dot{}}{1}=G\left(G\left(X\right)\right)$$
46	24 27 45	syl2anc	$$⊢\phi \to G\left(G\left(X\right)\right)\underset{\dot{}}{\times }\underset{\dot{}}{1}=G\left(G\left(X\right)\right)$$
47	41 44 46	3eqtrrd	$$⊢\phi \to G\left(G\left(X\right)\right)=\left(G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)$$
48	21	fveq2d	$$⊢\phi \to G\left(Y\underset{\dot{}}{\times }G\left(X\right)\right)=G\left(\underset{\dot{}}{1}\right)$$
49	1 4 7 8 9 14 15 28 26	hgmapmul	$$⊢\phi \to G\left(Y\underset{\dot{}}{\times }G\left(X\right)\right)=G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)$$
50	48 49	eqtr3d	$$⊢\phi \to G\left(\underset{\dot{}}{1}\right)=G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)$$
51	19	fveq2d	$$⊢\phi \to G\left(S\left(D\right)\left(C\right)\right)=G\left(\underset{\dot{}}{1}\right)$$
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	$$⊢\phi \to G\left(\underset{\dot{}}{1}\right)=S\left(C\right)\left(D\right)$$
56	50 55	eqtr3d	$$⊢\phi \to G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)=S\left(C\right)\left(D\right)$$
57	21 19	eqtr4d	$$⊢\phi \to Y\underset{\dot{}}{\times }G\left(X\right)=S\left(D\right)\left(C\right)$$
58	1 2 3 4 5 52 53 6 7 8 9 10 13 14 15 17 18 28 25 57	hdmapinvlem4	$$⊢\phi \to X\underset{\dot{}}{\times }G\left(Y\right)=S\left(C\right)\left(D\right)$$
59	56 58	eqtr4d	$$⊢\phi \to G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)=X\underset{\dot{}}{\times }G\left(Y\right)$$
60	59	oveq1d	$$⊢\phi \to \left(G\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=\left(X\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)$$
61	8 9	ringass	$$⊢\left(R\in \mathrm{Ring}\wedge \left(X\in B\wedge G\left(Y\right)\in B\wedge N\left(G\left(Y\right)\right)\in B\right)\right)\to \left(X\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=X\underset{\dot{}}{\times }\left(G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)\right)$$
62	24 25 29 39 61	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=X\underset{\dot{}}{\times }\left(G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)\right)$$
63	43	oveq2d	$$⊢\phi \to X\underset{\dot{}}{\times }\left(G\left(Y\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)\right)=X\underset{\dot{}}{\times }\underset{\dot{}}{1}$$
64	8 9 11	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\times }\underset{\dot{}}{1}=X$$
65	24 25 64	syl2anc	$$⊢\phi \to X\underset{\dot{}}{\times }\underset{\dot{}}{1}=X$$
66	62 63 65	3eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{\times }G\left(Y\right)\right)\underset{\dot{}}{\times }N\left(G\left(Y\right)\right)=X$$
67	47 60 66	3eqtrd	$$⊢\phi \to G\left(G\left(X\right)\right)=X$$