# 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 $⊢ H = LHyp ⁡ K$
hdmapinvlem3.e $⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W$
hdmapinvlem3.o $⊢ O = ocH ⁡ K ⁡ W$
hdmapinvlem3.u $⊢ U = DVecH ⁡ K ⁡ W$
hdmapinvlem3.v $⊢ V = Base U$
hdmapinvlem3.p
hdmapinvlem3.m
hdmapinvlem3.q
hdmapinvlem3.r $⊢ R = Scalar ⁡ U$
hdmapinvlem3.b $⊢ B = Base R$
hdmapinvlem3.t
hdmapinvlem3.z
hdmapinvlem3.s $⊢ S = HDMap ⁡ K ⁡ W$
hdmapinvlem3.g $⊢ G = HGMap ⁡ K ⁡ W$
hdmapinvlem3.k $⊢ φ → K ∈ HL ∧ W ∈ H$
hdmapinvlem3.c $⊢ φ → C ∈ O ⁡ E$
hdmapinvlem3.d $⊢ φ → D ∈ O ⁡ E$
hdmapinvlem3.i $⊢ φ → I ∈ B$
hdmapinvlem3.j $⊢ φ → J ∈ B$
hdmapinvlem3.ij
Assertion hdmapinvlem4

### Proof

Step Hyp Ref Expression
1 hdmapinvlem3.h $⊢ H = LHyp ⁡ K$
2 hdmapinvlem3.e $⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W$
3 hdmapinvlem3.o $⊢ O = ocH ⁡ K ⁡ W$
4 hdmapinvlem3.u $⊢ U = DVecH ⁡ K ⁡ W$
5 hdmapinvlem3.v $⊢ V = Base U$
6 hdmapinvlem3.p
7 hdmapinvlem3.m
8 hdmapinvlem3.q
9 hdmapinvlem3.r $⊢ R = Scalar ⁡ U$
10 hdmapinvlem3.b $⊢ B = Base R$
11 hdmapinvlem3.t
12 hdmapinvlem3.z
13 hdmapinvlem3.s $⊢ S = HDMap ⁡ K ⁡ W$
14 hdmapinvlem3.g $⊢ G = HGMap ⁡ K ⁡ W$
15 hdmapinvlem3.k $⊢ φ → K ∈ HL ∧ W ∈ H$
16 hdmapinvlem3.c $⊢ φ → C ∈ O ⁡ E$
17 hdmapinvlem3.d $⊢ φ → D ∈ O ⁡ E$
18 hdmapinvlem3.i $⊢ φ → I ∈ B$
19 hdmapinvlem3.j $⊢ φ → J ∈ B$
20 hdmapinvlem3.ij
21 eqid $⊢ - R = - R$
22 1 4 15 dvhlmod $⊢ φ → U ∈ LMod$
23 eqid $⊢ Base K = Base K$
24 eqid $⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W$
25 eqid $⊢ 0 U = 0 U$
26 1 23 24 4 5 25 2 15 dvheveccl $⊢ φ → E ∈ V ∖ 0 U$
27 26 eldifad $⊢ φ → E ∈ V$
28 5 9 8 10 lmodvscl
29 22 19 27 28 syl3anc
30 27 snssd $⊢ φ → E ⊆ V$
31 1 4 5 3 dochssv $⊢ K ∈ HL ∧ W ∈ H ∧ E ⊆ V → O ⁡ E ⊆ V$
32 15 30 31 syl2anc $⊢ φ → O ⁡ E ⊆ V$
33 32 17 sseldd $⊢ φ → D ∈ V$
34 5 9 8 10 lmodvscl
35 22 18 27 34 syl3anc
36 32 16 sseldd $⊢ φ → C ∈ V$
37 5 6 lmodvacl
38 22 35 36 37 syl3anc
39 1 4 5 7 9 21 13 15 29 33 38 hdmaplns1
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 hdmapinvlem3
41 5 7 lmodvsubcl
42 22 29 33 41 syl3anc
43 1 4 5 9 12 13 15 42 38 hdmapip0com
44 40 43 mpbid
45 1 4 5 8 9 10 11 13 15 27 38 19 hdmaplnm1
46 eqid $⊢ + R = + R$
47 1 4 5 6 9 46 13 15 27 35 36 hdmaplna2
48 1 2 3 4 5 9 10 11 12 13 15 16 hdmapinvlem2
49 48 oveq2d
50 9 lmodring $⊢ U ∈ LMod → R ∈ Ring$
51 22 50 syl $⊢ φ → R ∈ Ring$
52 ringgrp $⊢ R ∈ Ring → R ∈ Grp$
53 51 52 syl $⊢ φ → R ∈ Grp$
54 1 4 5 9 10 13 15 27 35 hdmapipcl
55 10 46 12 grprid
56 53 54 55 syl2anc
57 1 4 5 8 9 10 11 13 14 15 27 27 18 hdmapglnm2
58 eqid $⊢ HVMap ⁡ K ⁡ W = HVMap ⁡ K ⁡ W$
59 eqid $⊢ 1 R = 1 R$
60 1 2 58 13 15 4 9 59 hdmapevec2 $⊢ φ → S ⁡ E ⁡ E = 1 R$
61 60 oveq1d
62 1 4 9 10 14 15 18 hgmapcl $⊢ φ → G ⁡ I ∈ B$
63 10 11 59 ringlidm
64 51 62 63 syl2anc
65 61 64 eqtrd
66 56 57 65 3eqtrd
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
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
73 72 oveq1d
74 10 11 12 ringlz
75 51 62 74 syl2anc
76 71 73 75 3eqtrd
77 76 oveq1d
78 1 4 5 9 10 13 15 33 36 hdmapipcl $⊢ φ → S ⁡ C ⁡ D ∈ B$
79 10 46 12 grplid
80 53 78 79 syl2anc
81 70 77 80 3eqtrd
82 69 81 oveq12d
83 39 44 82 3eqtr3rd
84 9 10 11 lmodmcl
85 22 19 62 84 syl3anc
86 10 12 21 grpsubeq0
87 53 85 78 86 syl3anc
88 83 87 mpbid