Metamath Proof Explorer


Theorem lcfrlem31

Description: Lemma for lcfr . (Contributed by NM, 10-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h H = LHyp K
lcfrlem17.o ˙ = ocH K W
lcfrlem17.u U = DVecH K W
lcfrlem17.v V = Base U
lcfrlem17.p + ˙ = + U
lcfrlem17.z 0 ˙ = 0 U
lcfrlem17.n N = LSpan U
lcfrlem17.a A = LSAtoms U
lcfrlem17.k φ K HL W H
lcfrlem17.x φ X V 0 ˙
lcfrlem17.y φ Y V 0 ˙
lcfrlem17.ne φ N X N Y
lcfrlem22.b B = N X Y ˙ X + ˙ Y
lcfrlem24.t · ˙ = U
lcfrlem24.s S = Scalar U
lcfrlem24.q Q = 0 S
lcfrlem24.r R = Base S
lcfrlem24.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
lcfrlem24.ib φ I B
lcfrlem24.l L = LKer U
lcfrlem25.d D = LDual U
lcfrlem28.jn φ J Y I Q
lcfrlem29.i F = inv r S
lcfrlem30.m - ˙ = - D
lcfrlem30.c C = J X - ˙ F J Y I S J X I D J Y
lcfrlem31.xi φ J X I Q
lcfrlem31.cn φ C = 0 D
Assertion lcfrlem31 φ N X = N Y

Proof

Step Hyp Ref Expression
1 lcfrlem17.h H = LHyp K
2 lcfrlem17.o ˙ = ocH K W
3 lcfrlem17.u U = DVecH K W
4 lcfrlem17.v V = Base U
5 lcfrlem17.p + ˙ = + U
6 lcfrlem17.z 0 ˙ = 0 U
7 lcfrlem17.n N = LSpan U
8 lcfrlem17.a A = LSAtoms U
9 lcfrlem17.k φ K HL W H
10 lcfrlem17.x φ X V 0 ˙
11 lcfrlem17.y φ Y V 0 ˙
12 lcfrlem17.ne φ N X N Y
13 lcfrlem22.b B = N X Y ˙ X + ˙ Y
14 lcfrlem24.t · ˙ = U
15 lcfrlem24.s S = Scalar U
16 lcfrlem24.q Q = 0 S
17 lcfrlem24.r R = Base S
18 lcfrlem24.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
19 lcfrlem24.ib φ I B
20 lcfrlem24.l L = LKer U
21 lcfrlem25.d D = LDual U
22 lcfrlem28.jn φ J Y I Q
23 lcfrlem29.i F = inv r S
24 lcfrlem30.m - ˙ = - D
25 lcfrlem30.c C = J X - ˙ F J Y I S J X I D J Y
26 lcfrlem31.xi φ J X I Q
27 lcfrlem31.cn φ C = 0 D
28 25 27 eqtr3id φ J X - ˙ F J Y I S J X I D J Y = 0 D
29 1 3 9 dvhlmod φ U LMod
30 21 29 lduallmod φ D LMod
31 eqid LFnl U = LFnl U
32 eqid Base D = Base D
33 eqid 0 D = 0 D
34 eqid f LFnl U | ˙ ˙ L f = L f = f LFnl U | ˙ ˙ L f = L f
35 1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 10 lcfrlem10 φ J X LFnl U
36 31 21 32 29 35 ldualelvbase φ J X Base D
37 eqid D = D
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 lcfrlem29 φ F J Y I S J X I R
39 1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 11 lcfrlem10 φ J Y LFnl U
40 31 15 17 21 37 29 38 39 ldualvscl φ F J Y I S J X I D J Y LFnl U
41 31 21 32 29 40 ldualelvbase φ F J Y I S J X I D J Y Base D
42 32 33 24 lmodsubeq0 D LMod J X Base D F J Y I S J X I D J Y Base D J X - ˙ F J Y I S J X I D J Y = 0 D J X = F J Y I S J X I D J Y
43 30 36 41 42 syl3anc φ J X - ˙ F J Y I S J X I D J Y = 0 D J X = F J Y I S J X I D J Y
44 28 43 mpbid φ J X = F J Y I S J X I D J Y
45 44 fveq2d φ L J X = L F J Y I S J X I D J Y
46 1 3 9 dvhlvec φ U LVec
47 15 lvecdrng U LVec S DivRing
48 46 47 syl φ S DivRing
49 1 2 3 4 5 6 7 8 9 10 11 12 13 lcfrlem22 φ B A
50 4 8 29 49 lsatssv φ B V
51 50 19 sseldd φ I V
52 15 17 4 31 lflcl U LMod J Y LFnl U I V J Y I R
53 29 39 51 52 syl3anc φ J Y I R
54 17 16 23 drnginvrn0 S DivRing J Y I R J Y I Q F J Y I Q
55 48 53 22 54 syl3anc φ F J Y I Q
56 eqid S = S
57 17 16 23 drnginvrcl S DivRing J Y I R J Y I Q F J Y I R
58 48 53 22 57 syl3anc φ F J Y I R
59 15 17 4 31 lflcl U LMod J X LFnl U I V J X I R
60 29 35 51 59 syl3anc φ J X I R
61 17 16 56 48 58 60 drngmulne0 φ F J Y I S J X I Q F J Y I Q J X I Q
62 55 26 61 mpbir2and φ F J Y I S J X I Q
63 15 17 16 31 20 21 37 46 39 38 62 ldualkrsc φ L F J Y I S J X I D J Y = L J Y
64 45 63 eqtrd φ L J X = L J Y
65 64 fveq2d φ ˙ L J X = ˙ L J Y
66 1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 10 7 lcfrlem14 φ ˙ L J X = N X
67 1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 11 7 lcfrlem14 φ ˙ L J Y = N Y
68 65 66 67 3eqtr3d φ N X = N Y