Metamath Proof Explorer


Theorem hdmaprnlem3eN

Description: Lemma for hdmaprnN . (Contributed by NM, 29-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
hdmaprnlem3e.p + ˙ = + U
Assertion hdmaprnlem3eN φ t N v 0 ˙ L S u ˙ s = M N u + ˙ 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 hdmaprnlem3e.p + ˙ = + U
20 eqid LSAtoms U = LSAtoms U
21 1 2 9 dvhlvec φ U LVec
22 eqid LSAtoms C = LSAtoms C
23 1 5 9 lcdlmod φ C LMod
24 1 2 3 5 15 8 9 13 hdmapcl φ S u D
25 10 eldifad φ s D
26 15 18 lmodvacl C LMod S u D s D S u ˙ s D
27 23 24 25 26 syl3anc φ S u ˙ s D
28 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmaprnlem1N φ L S u L s
29 15 18 16 6 23 24 25 28 lmodindp1 φ S u ˙ s Q
30 eldifsn S u ˙ s D Q S u ˙ s D S u ˙ s Q
31 27 29 30 sylanbrc φ S u ˙ s D Q
32 15 6 16 22 23 31 lsatlspsn φ L S u ˙ s LSAtoms C
33 1 7 2 20 5 22 9 32 mapdcnvatN φ M -1 L S u ˙ s LSAtoms U
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmaprnlem3uN φ N u M -1 L S u ˙ s
35 34 necomd φ M -1 L S u ˙ s N u
36 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
37 36 necomd φ M -1 L S u ˙ s N v
38 eqid LSubSp C = LSubSp C
39 eqid LSubSp U = LSubSp U
40 1 2 9 dvhlmod φ U LMod
41 3 39 4 lspsncl U LMod u V N u LSubSp U
42 40 13 41 syl2anc φ N u LSubSp U
43 1 7 2 39 5 38 9 42 mapdcl2 φ M N u LSubSp C
44 3 39 4 lspsncl U LMod v V N v LSubSp U
45 40 11 44 syl2anc φ N v LSubSp U
46 1 7 2 39 5 38 9 45 mapdcl2 φ M N v LSubSp C
47 eqid LSSum C = LSSum C
48 38 47 lsmcl C LMod M N u LSubSp C M N v LSubSp C M N u LSSum C M N v LSubSp C
49 23 43 46 48 syl3anc φ M N u LSSum C M N v LSubSp C
50 38 lsssssubg C LMod LSubSp C SubGrp C
51 23 50 syl φ LSubSp C SubGrp C
52 51 43 sseldd φ M N u SubGrp C
53 51 46 sseldd φ M N v SubGrp C
54 15 6 lspsnid C LMod S u D S u L S u
55 23 24 54 syl2anc φ S u L S u
56 1 2 3 4 5 6 7 8 9 13 hdmap10 φ M N u = L S u
57 55 56 eleqtrrd φ S u M N u
58 eqimss2 M N v = L s L s M N v
59 12 58 syl φ L s M N v
60 15 38 6 23 46 25 lspsnel5 φ s M N v L s M N v
61 59 60 mpbird φ s M N v
62 18 47 lsmelvali M N u SubGrp C M N v SubGrp C S u M N u s M N v S u ˙ s M N u LSSum C M N v
63 52 53 57 61 62 syl22anc φ S u ˙ s M N u LSSum C M N v
64 38 6 23 49 63 lspsnel5a φ L S u ˙ s M N u LSSum C M N v
65 eqid LSSum U = LSSum U
66 1 7 2 39 65 5 47 9 42 45 mapdlsm φ M N u LSSum U N v = M N u LSSum C M N v
67 64 66 sseqtrrd φ L S u ˙ s M N u LSSum U N v
68 15 38 6 lspsncl C LMod S u ˙ s D L S u ˙ s LSubSp C
69 23 27 68 syl2anc φ L S u ˙ s LSubSp C
70 1 7 5 38 9 mapdrn2 φ ran M = LSubSp C
71 69 70 eleqtrrd φ L S u ˙ s ran M
72 39 65 lsmcl U LMod N u LSubSp U N v LSubSp U N u LSSum U N v LSubSp U
73 40 42 45 72 syl3anc φ N u LSSum U N v LSubSp U
74 1 7 2 39 9 73 mapdcl φ M N u LSSum U N v ran M
75 1 7 9 71 74 mapdcnvordN φ M -1 L S u ˙ s M -1 M N u LSSum U N v L S u ˙ s M N u LSSum U N v
76 67 75 mpbird φ M -1 L S u ˙ s M -1 M N u LSSum U N v
77 3 4 65 40 13 11 lsmpr φ N u v = N u LSSum U N v
78 1 7 2 39 9 73 mapdcnvid1N φ M -1 M N u LSSum U N v = N u LSSum U N v
79 77 78 eqtr4d φ N u v = M -1 M N u LSSum U N v
80 76 79 sseqtrrd φ M -1 L S u ˙ s N u v
81 3 19 17 4 20 21 33 13 11 35 37 80 lsatfixedN φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t
82 simpr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t M -1 L S u ˙ s = N u + ˙ t
83 9 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t K HL W H
84 40 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t U LMod
85 13 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t u V
86 10 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t s D Q
87 11 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t v V
88 12 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t M N v = L s
89 14 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t ¬ u N v
90 simplr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t t N v 0 ˙
91 1 2 3 4 5 6 7 8 83 86 87 88 85 89 15 16 17 18 90 hdmaprnlem4tN φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t t V
92 3 19 lmodvacl U LMod u V t V u + ˙ t V
93 84 85 91 92 syl3anc φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t u + ˙ t V
94 3 39 4 lspsncl U LMod u + ˙ t V N u + ˙ t LSubSp U
95 84 93 94 syl2anc φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t N u + ˙ t LSubSp U
96 1 7 2 39 83 95 mapdcnvid1N φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t M -1 M N u + ˙ t = N u + ˙ t
97 82 96 eqtr4d φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t M -1 L S u ˙ s = M -1 M N u + ˙ t
98 71 ad2antrr φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t L S u ˙ s ran M
99 1 7 2 39 83 95 mapdcl φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t M N u + ˙ t ran M
100 1 7 83 98 99 mapdcnv11N φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t M -1 L S u ˙ s = M -1 M N u + ˙ t L S u ˙ s = M N u + ˙ t
101 97 100 mpbid φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t L S u ˙ s = M N u + ˙ t
102 101 ex φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t L S u ˙ s = M N u + ˙ t
103 102 reximdva φ t N v 0 ˙ M -1 L S u ˙ s = N u + ˙ t t N v 0 ˙ L S u ˙ s = M N u + ˙ t
104 81 103 mpd φ t N v 0 ˙ L S u ˙ s = M N u + ˙ t