Metamath Proof Explorer


Theorem hdmaprnlem9N

Description: Part of proof of part 12 in Baer p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 and mapdcnv11N . Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmaprnlem1.h H = LHyp K
hdmaprnlem1.u U = DVecH K W
hdmaprnlem1.v V = Base U
hdmaprnlem1.n N = LSpan U
hdmaprnlem1.c C = LCDual K W
hdmaprnlem1.l L = LSpan C
hdmaprnlem1.m M = mapd K W
hdmaprnlem1.s S = HDMap K W
hdmaprnlem1.k φ K HL W H
hdmaprnlem1.se φ s D Q
hdmaprnlem1.ve φ v V
hdmaprnlem1.e φ M N v = L s
hdmaprnlem1.ue φ u V
hdmaprnlem1.un φ ¬ u N v
hdmaprnlem1.d D = Base C
hdmaprnlem1.q Q = 0 C
hdmaprnlem1.o 0 ˙ = 0 U
hdmaprnlem1.a ˙ = + C
hdmaprnlem1.t2 φ t N v 0 ˙
hdmaprnlem1.p + ˙ = + U
hdmaprnlem1.pt φ L S u ˙ s = M N u + ˙ t
Assertion hdmaprnlem9N φ s = S t

Proof

Step Hyp Ref Expression
1 hdmaprnlem1.h H = LHyp K
2 hdmaprnlem1.u U = DVecH K W
3 hdmaprnlem1.v V = Base U
4 hdmaprnlem1.n N = LSpan U
5 hdmaprnlem1.c C = LCDual K W
6 hdmaprnlem1.l L = LSpan C
7 hdmaprnlem1.m M = mapd K W
8 hdmaprnlem1.s S = HDMap K W
9 hdmaprnlem1.k φ K HL W H
10 hdmaprnlem1.se φ s D Q
11 hdmaprnlem1.ve φ v V
12 hdmaprnlem1.e φ M N v = L s
13 hdmaprnlem1.ue φ u V
14 hdmaprnlem1.un φ ¬ u N v
15 hdmaprnlem1.d D = Base C
16 hdmaprnlem1.q Q = 0 C
17 hdmaprnlem1.o 0 ˙ = 0 U
18 hdmaprnlem1.a ˙ = + C
19 hdmaprnlem1.t2 φ t N v 0 ˙
20 hdmaprnlem1.p + ˙ = + U
21 hdmaprnlem1.pt φ L S u ˙ s = M N u + ˙ t
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 hdmaprnlem7N φ s - C S t L S u ˙ s
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 hdmaprnlem8N φ s - C S t M N t
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 hdmaprnlem4N φ M N t = L s
25 23 24 eleqtrd φ s - C S t L s
26 22 25 elind φ s - C S t L S u ˙ s L s
27 1 5 9 lcdlvec φ C LVec
28 1 5 9 lcdlmod φ C LMod
29 1 2 3 5 15 8 9 13 hdmapcl φ S u D
30 10 eldifad φ s D
31 15 18 lmodvacl C LMod S u D s D S u ˙ s D
32 28 29 30 31 syl3anc φ S u ˙ s D
33 eqid LSubSp C = LSubSp C
34 15 33 6 lspsncl C LMod s D L s LSubSp C
35 28 30 34 syl2anc φ L s LSubSp C
36 1 7 5 33 9 mapdrn2 φ ran M = LSubSp C
37 35 36 eleqtrrd φ L s ran M
38 1 7 9 37 mapdcnvid2 φ M M -1 L s = L s
39 12 38 eqtr4d φ M N v = M M -1 L s
40 eqid LSubSp U = LSubSp U
41 1 2 9 dvhlmod φ U LMod
42 3 40 4 lspsncl U LMod v V N v LSubSp U
43 41 11 42 syl2anc φ N v LSubSp U
44 1 7 2 40 9 37 mapdcnvcl φ M -1 L s LSubSp U
45 1 2 40 7 9 43 44 mapd11 φ M N v = M M -1 L s N v = M -1 L s
46 39 45 mpbid φ N v = M -1 L s
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmaprnlem3N φ N v M -1 L S u ˙ s
48 46 47 eqnetrrd φ M -1 L s M -1 L S u ˙ s
49 15 33 6 lspsncl C LMod S u ˙ s D L S u ˙ s LSubSp C
50 28 32 49 syl2anc φ L S u ˙ s LSubSp C
51 50 36 eleqtrrd φ L S u ˙ s ran M
52 1 7 9 37 51 mapdcnv11N φ M -1 L s = M -1 L S u ˙ s L s = L S u ˙ s
53 52 necon3bid φ M -1 L s M -1 L S u ˙ s L s L S u ˙ s
54 48 53 mpbid φ L s L S u ˙ s
55 54 necomd φ L S u ˙ s L s
56 15 16 6 27 32 30 55 lspdisj2 φ L S u ˙ s L s = Q
57 26 56 eleqtrd φ s - C S t Q
58 elsni s - C S t Q s - C S t = Q
59 57 58 syl φ s - C S t = Q
60 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 hdmaprnlem4tN φ t V
61 1 2 3 5 15 8 9 60 hdmapcl φ S t D
62 eqid - C = - C
63 15 16 62 lmodsubeq0 C LMod s D S t D s - C S t = Q s = S t
64 28 30 61 63 syl3anc φ s - C S t = Q s = S t
65 59 64 mpbid φ s = S t