Metamath Proof Explorer


Theorem baerlem5blem2

Description: Lemma for baerlem5b . (Contributed by NM, 13-Apr-2015)

Ref Expression
Hypotheses baerlem3.v V=BaseW
baerlem3.m -˙=-W
baerlem3.o 0˙=0W
baerlem3.s ˙=LSSumW
baerlem3.n N=LSpanW
baerlem3.w φWLVec
baerlem3.x φXV
baerlem3.c φ¬XNYZ
baerlem3.d φNYNZ
baerlem3.y φYV0˙
baerlem3.z φZV0˙
baerlem3.p +˙=+W
baerlem3.t ·˙=W
baerlem3.r R=ScalarW
baerlem3.b B=BaseR
baerlem3.a ˙=+R
baerlem3.l L=-R
baerlem3.q Q=0R
baerlem3.i I=invgR
Assertion baerlem5blem2 φNY+˙Z=NY˙NZNX-˙Y+˙Z˙NX

Proof

Step Hyp Ref Expression
1 baerlem3.v V=BaseW
2 baerlem3.m -˙=-W
3 baerlem3.o 0˙=0W
4 baerlem3.s ˙=LSSumW
5 baerlem3.n N=LSpanW
6 baerlem3.w φWLVec
7 baerlem3.x φXV
8 baerlem3.c φ¬XNYZ
9 baerlem3.d φNYNZ
10 baerlem3.y φYV0˙
11 baerlem3.z φZV0˙
12 baerlem3.p +˙=+W
13 baerlem3.t ·˙=W
14 baerlem3.r R=ScalarW
15 baerlem3.b B=BaseR
16 baerlem3.a ˙=+R
17 baerlem3.l L=-R
18 baerlem3.q Q=0R
19 baerlem3.i I=invgR
20 lveclmod WLVecWLMod
21 6 20 syl φWLMod
22 10 eldifad φYV
23 11 eldifad φZV
24 1 12 5 4 lspsntri WLModYVZVNY+˙ZNY˙NZ
25 21 22 23 24 syl3anc φNY+˙ZNY˙NZ
26 1 12 lmodvacl WLModYVZVY+˙ZV
27 21 22 23 26 syl3anc φY+˙ZV
28 1 2 lmodvsubcl WLModXVY+˙ZVX-˙Y+˙ZV
29 21 7 27 28 syl3anc φX-˙Y+˙ZV
30 1 2 5 21 29 7 lspsnsub φNX-˙Y+˙Z-˙X=NX-˙X-˙Y+˙Z
31 lmodabl WLModWAbel
32 21 31 syl φWAbel
33 1 2 32 7 27 ablnncan φX-˙X-˙Y+˙Z=Y+˙Z
34 33 sneqd φX-˙X-˙Y+˙Z=Y+˙Z
35 34 fveq2d φNX-˙X-˙Y+˙Z=NY+˙Z
36 30 35 eqtrd φNX-˙Y+˙Z-˙X=NY+˙Z
37 1 2 4 5 lspsntrim WLModX-˙Y+˙ZVXVNX-˙Y+˙Z-˙XNX-˙Y+˙Z˙NX
38 21 29 7 37 syl3anc φNX-˙Y+˙Z-˙XNX-˙Y+˙Z˙NX
39 36 38 eqsstrrd φNY+˙ZNX-˙Y+˙Z˙NX
40 25 39 ssind φNY+˙ZNY˙NZNX-˙Y+˙Z˙NX
41 elin jNY˙NZNX-˙Y+˙Z˙NXjNY˙NZjNX-˙Y+˙Z˙NX
42 1 12 14 15 13 4 5 21 22 23 lsmspsn φjNY˙NZaBbBj=a·˙Y+˙b·˙Z
43 1 12 14 15 13 4 5 21 29 7 lsmspsn φjNX-˙Y+˙Z˙NXdBeBj=d·˙X-˙Y+˙Z+˙e·˙X
44 42 43 anbi12d φjNY˙NZjNX-˙Y+˙Z˙NXaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙X
45 41 44 syl5bb φjNY˙NZNX-˙Y+˙Z˙NXaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙X
46 simp11 φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙Xφ
47 46 6 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XWLVec
48 46 7 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XXV
49 46 8 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙X¬XNYZ
50 46 9 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XNYNZ
51 46 10 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XYV0˙
52 46 11 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XZV0˙
53 simp12l φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XaB
54 simp12r φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XbB
55 simp2l φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XdB
56 simp2r φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XeB
57 simp13 φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙Xj=a·˙Y+˙b·˙Z
58 simp3 φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙Xj=d·˙X-˙Y+˙Z+˙e·˙X
59 1 2 3 4 5 47 48 49 50 51 52 12 13 14 15 16 17 18 19 53 54 55 56 57 58 baerlem5blem1 φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙Xj=Id·˙Y+˙Z
60 46 21 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XWLMod
61 14 lmodring WLModRRing
62 ringgrp RRingRGrp
63 46 21 61 62 4syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XRGrp
64 15 19 grpinvcl RGrpdBIdB
65 63 55 64 syl2anc φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XIdB
66 46 27 syl φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XY+˙ZV
67 1 13 14 15 5 60 65 66 lspsneli φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XId·˙Y+˙ZNY+˙Z
68 59 67 eqeltrd φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XjNY+˙Z
69 68 3exp φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XjNY+˙Z
70 69 rexlimdvv φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XjNY+˙Z
71 70 3exp φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XjNY+˙Z
72 71 rexlimdvv φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XjNY+˙Z
73 72 impd φaBbBj=a·˙Y+˙b·˙ZdBeBj=d·˙X-˙Y+˙Z+˙e·˙XjNY+˙Z
74 45 73 sylbid φjNY˙NZNX-˙Y+˙Z˙NXjNY+˙Z
75 74 ssrdv φNY˙NZNX-˙Y+˙Z˙NXNY+˙Z
76 40 75 eqssd φNY+˙Z=NY˙NZNX-˙Y+˙Z˙NX