Metamath Proof Explorer


Theorem hdmaprnlem3N

Description: Part of proof of part 12 in Baer p. 49 line 15, T =/= P. Our (`' M `( L{ ( ( Su ) .+b s ) } ) ) is Baer's P, where P* = G(u'+s). (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
Assertion hdmaprnlem3N φ N v M -1 L S u ˙ 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 hdmaprnlem1.d D = Base C
16 hdmaprnlem1.q Q = 0 C
17 hdmaprnlem1.o 0 ˙ = 0 U
18 hdmaprnlem1.a ˙ = + C
19 1 5 9 lcdlmod φ C LMod
20 1 2 3 5 15 8 9 13 hdmapcl φ S u D
21 10 eldifad φ s D
22 15 18 lmodvacl C LMod S u D s D S u ˙ s D
23 19 20 21 22 syl3anc φ S u ˙ s D
24 eqid LSubSp C = LSubSp C
25 15 24 6 lspsncl C LMod s D L s LSubSp C
26 19 21 25 syl2anc φ L s LSubSp C
27 15 6 lspsnid C LMod s D s L s
28 19 21 27 syl2anc φ s L s
29 1 5 9 lcdlvec φ C LVec
30 eqid LSubSp U = LSubSp U
31 1 2 9 dvhlmod φ U LMod
32 3 30 4 lspsncl U LMod v V N v LSubSp U
33 31 11 32 syl2anc φ N v LSubSp U
34 17 30 31 33 13 14 lssneln0 φ u V 0 ˙
35 1 2 3 17 5 16 15 8 9 34 hdmapnzcl φ S u D Q
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmaprnlem1N φ L S u L s
37 15 16 6 29 35 21 36 lspsnne1 φ ¬ S u L s
38 15 18 24 19 26 28 20 37 lssvancl2 φ ¬ S u ˙ s L s
39 15 6 19 23 21 38 lspsnne2 φ L S u ˙ s L s
40 39 necomd φ L s L S u ˙ s
41 15 24 6 lspsncl C LMod S u ˙ s D L S u ˙ s LSubSp C
42 19 23 41 syl2anc φ L S u ˙ s LSubSp C
43 1 7 5 24 9 mapdrn2 φ ran M = LSubSp C
44 42 43 eleqtrrd φ L S u ˙ s ran M
45 1 7 9 44 mapdcnvid2 φ M M -1 L S u ˙ s = L S u ˙ s
46 40 12 45 3netr4d φ M N v M M -1 L S u ˙ s
47 1 7 2 30 9 44 mapdcnvcl φ M -1 L S u ˙ s LSubSp U
48 1 2 30 7 9 33 47 mapd11 φ M N v = M M -1 L S u ˙ s N v = M -1 L S u ˙ s
49 48 necon3bid φ M N v M M -1 L S u ˙ s N v M -1 L S u ˙ s
50 46 49 mpbid φ N v M -1 L S u ˙ s