Metamath Proof Explorer


Theorem hdmaprnlem8N

Description: Part of proof of part 12 in Baer p. 49 line 19, s-St e. (Ft)* = T*. (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 hdmaprnlem8N φ s - C S t M N 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 5 9 lcdlmod φ C LMod
23 eqid LSubSp U = LSubSp U
24 eqid LSubSp C = LSubSp C
25 1 2 9 dvhlmod φ U LMod
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 hdmaprnlem4tN φ t V
27 3 23 4 lspsncl U LMod t V N t LSubSp U
28 25 26 27 syl2anc φ N t LSubSp U
29 1 7 2 23 5 24 9 28 mapdcl2 φ M N t LSubSp C
30 10 eldifad φ s D
31 15 6 lspsnid C LMod s D s L s
32 22 30 31 syl2anc φ s L s
33 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
34 32 33 eleqtrrd φ s M N t
35 1 2 3 5 15 8 9 26 hdmapcl φ S t D
36 15 6 lspsnid C LMod S t D S t L S t
37 22 35 36 syl2anc φ S t L S t
38 1 2 3 4 5 6 7 8 9 26 hdmap10 φ M N t = L S t
39 37 38 eleqtrrd φ S t M N t
40 eqid - C = - C
41 40 24 lssvsubcl C LMod M N t LSubSp C s M N t S t M N t s - C S t M N t
42 22 29 34 39 41 syl22anc φ s - C S t M N t