Metamath Proof Explorer


Theorem hdmaprnlem1N

Description: Part of proof of part 12 in Baer p. 49 line 10, Gu' =/= Gs. Our ( N{ v } ) is Baer's T. (Contributed by NM, 26-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
Assertion hdmaprnlem1N φ L S u L s

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 1 2 9 dvhlmod φ U LMod
16 3 4 15 13 11 14 lspsnne2 φ N u N v
17 eqid LSubSp U = LSubSp U
18 3 17 4 lspsncl U LMod u V N u LSubSp U
19 15 13 18 syl2anc φ N u LSubSp U
20 3 17 4 lspsncl U LMod v V N v LSubSp U
21 15 11 20 syl2anc φ N v LSubSp U
22 1 2 17 7 9 19 21 mapd11 φ M N u = M N v N u = N v
23 22 necon3bid φ M N u M N v N u N v
24 16 23 mpbird φ M N u M N v
25 1 2 3 4 5 6 7 8 9 13 hdmap10 φ M N u = L S u
26 24 25 12 3netr3d φ L S u L s