Metamath Proof Explorer

Theorem hdmapinvlem3

Description: Line 30 in Baer p. 110, f(sw + u, tw - v) = 0. (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 hdmapinvlem3 ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = 0 )

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 ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
22 eqid ⊢ ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
23 1 4 15 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
24 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
25 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
26 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
27 1 24 25 4 5 26 2 15 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
28 27 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
29 5 9 8 10 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐽 · 𝐸 ) ∈ 𝑉 )
30 23 19 28 29 syl3anc ⊢ ( 𝜑 → ( 𝐽 · 𝐸 ) ∈ 𝑉 )
31 28 snssd ⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
32 1 4 5 3 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
33 15 31 32 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
34 33 17 sseldd ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
35 1 4 5 7 21 22 13 15 30 34 hdmapsub ⊢ ( 𝜑 → ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝐷 ) ) )
36 35 fveq1d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) )
37 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
38 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
39 1 4 5 21 38 13 15 30 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
40 1 4 5 21 38 13 15 34 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐷 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
41 5 9 8 10 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐼 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐼 · 𝐸 ) ∈ 𝑉 )
42 23 18 28 41 syl3anc ⊢ ( 𝜑 → ( 𝐼 · 𝐸 ) ∈ 𝑉 )
43 33 16 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
44 5 6 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 · 𝐸 ) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐼 · 𝐸 ) + 𝐶 ) ∈ 𝑉 )
45 23 42 43 44 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 · 𝐸 ) + 𝐶 ) ∈ 𝑉 )
46 1 4 5 9 37 21 38 22 15 39 40 45 lcdvsubval ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐷 ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ) )
47 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
48 1 4 5 6 9 47 13 15 42 43 30 hdmaplna1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( 𝐼 · 𝐸 ) ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ 𝐶 ) ) )
49 1 4 5 8 9 10 11 13 14 15 42 28 19 hdmapglnm2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( 𝐼 · 𝐸 ) ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ ( 𝐼 · 𝐸 ) ) × ( 𝐺 ‘ 𝐽 ) ) )
50 1 4 5 8 9 10 11 13 15 28 28 18 hdmaplnm1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ ( 𝐼 · 𝐸 ) ) = ( 𝐼 × ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) ) )
51 eqid ⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
52 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
53 1 2 51 13 15 4 9 52 hdmapevec2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = ( 1r ‘ 𝑅 ) )
54 53 oveq2d ⊢ ( 𝜑 → ( 𝐼 × ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) ) = ( 𝐼 × ( 1r ‘ 𝑅 ) ) )
55 9 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
56 23 55 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
57 10 11 52 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝐵 ) → ( 𝐼 × ( 1r ‘ 𝑅 ) ) = 𝐼 )
58 56 18 57 syl2anc ⊢ ( 𝜑 → ( 𝐼 × ( 1r ‘ 𝑅 ) ) = 𝐼 )
59 50 54 58 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ ( 𝐼 · 𝐸 ) ) = 𝐼 )
60 59 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ ( 𝐼 · 𝐸 ) ) × ( 𝐺 ‘ 𝐽 ) ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
61 49 60 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( 𝐼 · 𝐸 ) ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
62 1 4 5 8 9 10 11 13 14 15 43 28 19 hdmapglnm2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ 𝐶 ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) × ( 𝐺 ‘ 𝐽 ) ) )
63 1 2 3 4 5 9 10 11 12 13 15 16 hdmapinvlem1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) = 0 )
64 63 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) × ( 𝐺 ‘ 𝐽 ) ) = ( 0 × ( 𝐺 ‘ 𝐽 ) ) )
65 1 4 9 10 14 15 19 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐽 ) ∈ 𝐵 )
66 10 11 12 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝐽 ) ∈ 𝐵 ) → ( 0 × ( 𝐺 ‘ 𝐽 ) ) = 0 )
67 56 65 66 syl2anc ⊢ ( 𝜑 → ( 0 × ( 𝐺 ‘ 𝐽 ) ) = 0 )
68 62 64 67 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ 𝐶 ) = 0 )
69 61 68 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( 𝐼 · 𝐸 ) ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ 𝐶 ) ) = ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( +g ‘ 𝑅 ) 0 ) )
70 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
71 56 70 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
72 9 10 11 lmodmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐼 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝐽 ) ∈ 𝐵 ) → ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ∈ 𝐵 )
73 23 18 65 72 syl3anc ⊢ ( 𝜑 → ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ∈ 𝐵 )
74 10 47 12 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ∈ 𝐵 ) → ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( +g ‘ 𝑅 ) 0 ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
75 71 73 74 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( +g ‘ 𝑅 ) 0 ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
76 48 69 75 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
77 1 4 5 6 9 47 13 15 42 43 34 hdmaplna1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( ( ( 𝑆 ‘ 𝐷 ) ‘ ( 𝐼 · 𝐸 ) ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) )
78 1 4 5 8 9 10 11 13 15 28 34 18 hdmaplnm1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ ( 𝐼 · 𝐸 ) ) = ( 𝐼 × ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐸 ) ) )
79 1 2 3 4 5 9 10 11 12 13 15 17 hdmapinvlem2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐸 ) = 0 )
80 79 oveq2d ⊢ ( 𝜑 → ( 𝐼 × ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐸 ) ) = ( 𝐼 × 0 ) )
81 10 11 12 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝐵 ) → ( 𝐼 × 0 ) = 0 )
82 56 18 81 syl2anc ⊢ ( 𝜑 → ( 𝐼 × 0 ) = 0 )
83 78 80 82 3eqtrrd ⊢ ( 𝜑 → 0 = ( ( 𝑆 ‘ 𝐷 ) ‘ ( 𝐼 · 𝐸 ) ) )
84 83 20 oveq12d ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) = ( ( ( 𝑆 ‘ 𝐷 ) ‘ ( 𝐼 · 𝐸 ) ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) )
85 10 47 12 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
86 71 73 85 syl2anc ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
87 77 84 86 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) )
88 76 87 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐷 ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ) = ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( -g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) )
89 46 88 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( 𝑆 ‘ 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( -g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) )
90 10 12 37 grpsubid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ∈ 𝐵 ) → ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( -g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) = 0 )
91 71 73 90 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ( -g ‘ 𝑅 ) ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) ) = 0 )
92 36 89 91 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = 0 )