Metamath Proof Explorer

Theorem hdmapinvlem4

Description: Part 1.1 of Proposition 1 of Baer p. 110. We use C , D , I , and J for Baer's u, v, s, and t. Our unit vector E has the required properties for his w by hdmapevec2 . Our ( ( SD )C ) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hdmapinvlem3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapinvlem3.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapinvlem3.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hdmapinvlem3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapinvlem3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapinvlem3.p ⊢ + = ( +g ‘ 𝑈 )
hdmapinvlem3.m ⊢ − = ( -g ‘ 𝑈 )
hdmapinvlem3.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmapinvlem3.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapinvlem3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmapinvlem3.t ⊢ × = ( .r ‘ 𝑅 )
hdmapinvlem3.z ⊢ 0 = ( 0g ‘ 𝑅 )
hdmapinvlem3.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapinvlem3.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapinvlem3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapinvlem3.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapinvlem3.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapinvlem3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
hdmapinvlem3.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
hdmapinvlem3.ij ⊢ ( 𝜑 → ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
Assertion hdmapinvlem4 ( 𝜑 → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 hdmapinvlem3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapinvlem3.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapinvlem3.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapinvlem3.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapinvlem3.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 hdmapinvlem3.p ⊢ + = ( +g ‘ 𝑈 )
7 hdmapinvlem3.m ⊢ − = ( -g ‘ 𝑈 )
8 hdmapinvlem3.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
9 hdmapinvlem3.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
10 hdmapinvlem3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
11 hdmapinvlem3.t ⊢ × = ( .r ‘ 𝑅 )
12 hdmapinvlem3.z ⊢ 0 = ( 0g ‘ 𝑅 )
13 hdmapinvlem3.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
14 hdmapinvlem3.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
15 hdmapinvlem3.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 hdmapinvlem3.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
17 hdmapinvlem3.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
18 hdmapinvlem3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
19 hdmapinvlem3.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
20 hdmapinvlem3.ij ⊢ ( 𝜑 → ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
21 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
22 1 4 15 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
23 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
25 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
26 1 23 24 4 5 25 2 15 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
27 26 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
28 5 9 8 10 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐽 · 𝐸 ) ∈ 𝑉 )
29 22 19 27 28 syl3anc ⊢ ( 𝜑 → ( 𝐽 · 𝐸 ) ∈ 𝑉 )
30 27 snssd ⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
31 1 4 5 3 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
32 15 30 31 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
33 32 17 sseldd ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
34 5 9 8 10 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐼 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐼 · 𝐸 ) ∈ 𝑉 )
35 22 18 27 34 syl3anc ⊢ ( 𝜑 → ( 𝐼 · 𝐸 ) ∈ 𝑉 )
36 32 16 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
37 5 6 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 · 𝐸 ) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐼 · 𝐸 ) + 𝐶 ) ∈ 𝑉 )
38 22 35 36 37 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 · 𝐸 ) + 𝐶 ) ∈ 𝑉 )
39 1 4 5 7 9 21 13 15 29 33 38 hdmaplns1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = ( ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) ) )
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 hdmapinvlem3 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = 0 )
41 5 7 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐽 · 𝐸 ) ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝐽 · 𝐸 ) − 𝐷 ) ∈ 𝑉 )
42 22 29 33 41 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 · 𝐸 ) − 𝐷 ) ∈ 𝑉 )
43 1 4 5 9 12 13 15 42 38 hdmapip0com ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = 0 ↔ ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = 0 ) )
44 40 43 mpbid ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = 0 )
45 1 4 5 8 9 10 11 13 15 27 38 19 hdmaplnm1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) = ( 𝐽 × ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) ) )
46 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
47 1 4 5 6 9 46 13 15 27 35 36 hdmaplna2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) = ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
48 1 2 3 4 5 9 10 11 12 13 15 16 hdmapinvlem2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) = 0 )
49 48 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) )
50 9 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
51 22 50 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
52 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
53 51 52 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
54 1 4 5 9 10 13 15 27 35 hdmapipcl ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ∈ 𝐵 )
55 10 46 12 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ∈ 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) = ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) )
56 53 54 55 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) = ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) )
57 1 4 5 8 9 10 11 13 14 15 27 27 18 hdmapglnm2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) × ( 𝐺 ‘ 𝐼 ) ) )
58 eqid ⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
59 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
60 1 2 58 13 15 4 9 59 hdmapevec2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = ( 1r ‘ 𝑅 ) )
61 60 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) × ( 𝐺 ‘ 𝐼 ) ) = ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ 𝐼 ) ) )
62 1 4 9 10 14 15 18 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 )
63 10 11 59 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 𝐺 ‘ 𝐼 ) )
64 51 62 63 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 𝐺 ‘ 𝐼 ) )
65 61 64 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 𝐺 ‘ 𝐼 ) )
66 56 57 65 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) = ( 𝐺 ‘ 𝐼 ) )
67 47 49 66 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) = ( 𝐺 ‘ 𝐼 ) )
68 67 oveq2d ⊢ ( 𝜑 → ( 𝐽 × ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) ) = ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) )
69 45 68 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) = ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) )
70 1 4 5 6 9 46 13 15 33 35 36 hdmaplna2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) = ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
71 1 4 5 8 9 10 11 13 14 15 33 27 18 hdmapglnm2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐷 ) × ( 𝐺 ‘ 𝐼 ) ) )
72 1 2 3 4 5 9 10 11 12 13 15 17 hdmapinvlem1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐷 ) = 0 )
73 72 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐷 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 0 × ( 𝐺 ‘ 𝐼 ) ) )
74 10 11 12 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 ) → ( 0 × ( 𝐺 ‘ 𝐼 ) ) = 0 )
75 51 62 74 syl2anc ⊢ ( 𝜑 → ( 0 × ( 𝐺 ‘ 𝐼 ) ) = 0 )
76 71 73 75 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) = 0 )
77 76 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = ( 0 ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
78 1 4 5 9 10 13 15 33 36 hdmapipcl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ∈ 𝐵 )
79 10 46 12 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
80 53 78 79 syl2anc ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
81 70 77 80 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
82 69 81 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) ) = ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
83 39 44 82 3eqtr3rd ⊢ ( 𝜑 → ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = 0 )
84 9 10 11 lmodmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 ) → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐵 )
85 22 19 62 84 syl3anc ⊢ ( 𝜑 → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐵 )
86 10 12 21 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐵 ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ∈ 𝐵 ) → ( ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = 0 ↔ ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
87 53 85 78 86 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = 0 ↔ ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
88 83 87 mpbid ⊢ ( 𝜑 → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )