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 ⊢ 𝐻 = ( 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 ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )