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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapglem6.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapglem6.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapglem6.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapglem6.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapglem6.q	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hdmapglem6.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapglem6.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmapglem6.t	⊢ × = ( .r ‘ 𝑅 )
	hdmapglem6.z	⊢ 0 = ( 0g ‘ 𝑅 )
	hdmapglem6.i	⊢ 1 = ( 1r ‘ 𝑅 )
	hdmapglem6.n	⊢ 𝑁 = ( invr ‘ 𝑅 )
	hdmapglem6.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapglem6.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapglem6.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapglem6.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
	hdmapglem6.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
	hdmapglem6.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
	hdmapglem6.cd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) = 1 )
	hdmapglem6.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
	hdmapglem6.yx	⊢ ( 𝜑 → ( 𝑌 × ( 𝐺 ‘ 𝑋 ) ) = 1 )
Assertion	hgmapvvlem1	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		hdmapglem6.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapglem6.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapglem6.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapglem6.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapglem6.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		hdmapglem6.q	⊢ · = ( ·𝑠 ‘ 𝑈 )
7		hdmapglem6.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
8		hdmapglem6.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
9		hdmapglem6.t	⊢ × = ( .r ‘ 𝑅 )
10		hdmapglem6.z	⊢ 0 = ( 0g ‘ 𝑅 )
11		hdmapglem6.i	⊢ 1 = ( 1r ‘ 𝑅 )
12		hdmapglem6.n	⊢ 𝑁 = ( invr ‘ 𝑅 )
13		hdmapglem6.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
14		hdmapglem6.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
15		hdmapglem6.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16		hdmapglem6.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
17		hdmapglem6.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
18		hdmapglem6.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
19		hdmapglem6.cd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) = 1 )
20		hdmapglem6.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
21		hdmapglem6.yx	⊢ ( 𝜑 → ( 𝑌 × ( 𝐺 ‘ 𝑋 ) ) = 1 )
22	1 4 15	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
23	7	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
24	22 23	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
25	16	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
26	1 4 7 8 14 15 25	hgmapcl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐵 )
27	1 4 7 8 14 15 26	hgmapcl	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 )
28	20	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
29	1 4 7 8 14 15 28	hgmapcl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ∈ 𝐵 )
30	1 4 15	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
31	7	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
32	30 31	syl	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
33		eldifsni	⊢ ( 𝑌 ∈ ( 𝐵 ∖ { 0 } ) → 𝑌 ≠ 0 )
34	20 33	syl	⊢ ( 𝜑 → 𝑌 ≠ 0 )
35	1 4 7 8 10 14 15 28	hgmapeq0	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) = 0 ↔ 𝑌 = 0 ) )
36	35	necon3bid	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) ≠ 0 ↔ 𝑌 ≠ 0 ) )
37	34 36	mpbird	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ≠ 0 )
38	8 10 12	drnginvrcl	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑌 ) ≠ 0 ) → ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝐵 )
39	32 29 37 38	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝐵 )
40	8 9	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝐵 ) ) → ( ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑌 ) ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
41	24 27 29 39 40	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑌 ) ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
42	8 10 9 11 12	drnginvrr	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑌 ) ≠ 0 ) → ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = 1 )
43	32 29 37 42	syl3anc	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = 1 )
44	43	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) = ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × 1 ) )
45	8 9 11	ringridm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 ) → ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × 1 ) = ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) )
46	24 27 45	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × 1 ) = ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) )
47	41 44 46	3eqtrrd	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = ( ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑌 ) ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
48	21	fveq2d	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑌 × ( 𝐺 ‘ 𝑋 ) ) ) = ( 𝐺 ‘ 1 ) )
49	1 4 7 8 9 14 15 28 26	hgmapmul	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑌 × ( 𝐺 ‘ 𝑋 ) ) ) = ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑌 ) ) )
50	48 49	eqtr3d	⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = ( ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑌 ) ) )
51	19	fveq2d	⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) = ( 𝐺 ‘ 1 ) )
52		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
53		eqid	⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
54	1 2 3 4 5 52 53 6 7 8 9 10 13 14 15 17 18 28 25	hdmapglem5	⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
55	51 54	eqtr3d	⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
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	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ 𝐵 ) ) → ( ( 𝑋 × ( 𝐺 ‘ 𝑌 ) ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 𝑋 × ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
62	24 25 29 39 61	syl13anc	⊢ ( 𝜑 → ( ( 𝑋 × ( 𝐺 ‘ 𝑌 ) ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = ( 𝑋 × ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) )
63	43	oveq2d	⊢ ( 𝜑 → ( 𝑋 × ( ( 𝐺 ‘ 𝑌 ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) ) = ( 𝑋 × 1 ) )
64	8 9 11	ringridm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 × 1 ) = 𝑋 )
65	24 25 64	syl2anc	⊢ ( 𝜑 → ( 𝑋 × 1 ) = 𝑋 )
66	62 63 65	3eqtrd	⊢ ( 𝜑 → ( ( 𝑋 × ( 𝐺 ‘ 𝑌 ) ) × ( 𝑁 ‘ ( 𝐺 ‘ 𝑌 ) ) ) = 𝑋 )
67	47 60 66	3eqtrd	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )