Metamath Proof Explorer


Theorem baerlem5alem1

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

Ref Expression
Hypotheses baerlem3.v V = Base W
baerlem3.m - ˙ = - W
baerlem3.o 0 ˙ = 0 W
baerlem3.s ˙ = LSSum W
baerlem3.n N = LSpan W
baerlem3.w φ W LVec
baerlem3.x φ X V
baerlem3.c φ ¬ X N Y Z
baerlem3.d φ N Y N Z
baerlem3.y φ Y V 0 ˙
baerlem3.z φ Z V 0 ˙
baerlem3.p + ˙ = + W
baerlem3.t · ˙ = W
baerlem3.r R = Scalar W
baerlem3.b B = Base R
baerlem3.a ˙ = + R
baerlem3.l L = - R
baerlem3.q Q = 0 R
baerlem3.i I = inv g R
baerlem5a.a1 φ a B
baerlem5a.b1 φ b B
baerlem5a.d1 φ d B
baerlem5a.e1 φ e B
baerlem5a.j1 φ j = a · ˙ X - ˙ Y + ˙ b · ˙ Z
baerlem5a.j2 φ j = d · ˙ X - ˙ Z + ˙ e · ˙ Y
Assertion baerlem5alem1 φ j = a · ˙ X - ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 baerlem3.v V = Base W
2 baerlem3.m - ˙ = - W
3 baerlem3.o 0 ˙ = 0 W
4 baerlem3.s ˙ = LSSum W
5 baerlem3.n N = LSpan W
6 baerlem3.w φ W LVec
7 baerlem3.x φ X V
8 baerlem3.c φ ¬ X N Y Z
9 baerlem3.d φ N Y N Z
10 baerlem3.y φ Y V 0 ˙
11 baerlem3.z φ Z V 0 ˙
12 baerlem3.p + ˙ = + W
13 baerlem3.t · ˙ = W
14 baerlem3.r R = Scalar W
15 baerlem3.b B = Base R
16 baerlem3.a ˙ = + R
17 baerlem3.l L = - R
18 baerlem3.q Q = 0 R
19 baerlem3.i I = inv g R
20 baerlem5a.a1 φ a B
21 baerlem5a.b1 φ b B
22 baerlem5a.d1 φ d B
23 baerlem5a.e1 φ e B
24 baerlem5a.j1 φ j = a · ˙ X - ˙ Y + ˙ b · ˙ Z
25 baerlem5a.j2 φ j = d · ˙ X - ˙ Z + ˙ e · ˙ Y
26 lveclmod W LVec W LMod
27 6 26 syl φ W LMod
28 10 eldifad φ Y V
29 1 13 14 15 2 27 20 7 28 lmodsubdi φ a · ˙ X - ˙ Y = a · ˙ X - ˙ a · ˙ Y
30 1 14 13 15 lmodvscl W LMod a B X V a · ˙ X V
31 27 20 7 30 syl3anc φ a · ˙ X V
32 1 12 2 13 14 15 19 27 20 31 28 lmodsubvs φ a · ˙ X - ˙ a · ˙ Y = a · ˙ X + ˙ I a · ˙ Y
33 29 32 eqtrd φ a · ˙ X - ˙ Y = a · ˙ X + ˙ I a · ˙ Y
34 33 oveq1d φ a · ˙ X - ˙ Y + ˙ b · ˙ Z = a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z
35 14 lmodring W LMod R Ring
36 ringgrp R Ring R Grp
37 27 35 36 3syl φ R Grp
38 15 19 grpinvcl R Grp a B I a B
39 37 20 38 syl2anc φ I a B
40 1 14 13 15 lmodvscl W LMod I a B Y V I a · ˙ Y V
41 27 39 28 40 syl3anc φ I a · ˙ Y V
42 11 eldifad φ Z V
43 1 14 13 15 lmodvscl W LMod b B Z V b · ˙ Z V
44 27 21 42 43 syl3anc φ b · ˙ Z V
45 1 12 lmodass W LMod a · ˙ X V I a · ˙ Y V b · ˙ Z V a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z = a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z
46 27 31 41 44 45 syl13anc φ a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z = a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z
47 24 34 46 3eqtrd φ j = a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z
48 1 12 lmodvacl W LMod Y V Z V Y + ˙ Z V
49 27 28 42 48 syl3anc φ Y + ˙ Z V
50 1 14 13 15 lmodvscl W LMod a B Y + ˙ Z V a · ˙ Y + ˙ Z V
51 27 20 49 50 syl3anc φ a · ˙ Y + ˙ Z V
52 eqid inv g W = inv g W
53 1 12 52 2 grpsubval a · ˙ X V a · ˙ Y + ˙ Z V a · ˙ X - ˙ a · ˙ Y + ˙ Z = a · ˙ X + ˙ inv g W a · ˙ Y + ˙ Z
54 31 51 53 syl2anc φ a · ˙ X - ˙ a · ˙ Y + ˙ Z = a · ˙ X + ˙ inv g W a · ˙ Y + ˙ Z
55 1 13 14 15 2 27 20 7 49 lmodsubdi φ a · ˙ X - ˙ Y + ˙ Z = a · ˙ X - ˙ a · ˙ Y + ˙ Z
56 1 12 14 13 15 lmodvsdi W LMod I a B Y V Z V I a · ˙ Y + ˙ Z = I a · ˙ Y + ˙ I a · ˙ Z
57 27 39 28 42 56 syl13anc φ I a · ˙ Y + ˙ Z = I a · ˙ Y + ˙ I a · ˙ Z
58 1 14 13 52 15 19 27 49 20 lmodvsneg φ inv g W a · ˙ Y + ˙ Z = I a · ˙ Y + ˙ Z
59 15 19 grpinvcl R Grp d B I d B
60 37 22 59 syl2anc φ I d B
61 eqid LSubSp W = LSubSp W
62 1 61 5 27 28 42 lspprcl φ N Y Z LSubSp W
63 1 12 13 14 15 5 27 39 21 28 42 lsppreli φ I a · ˙ Y + ˙ b · ˙ Z N Y Z
64 1 12 13 14 15 5 27 23 60 28 42 lsppreli φ e · ˙ Y + ˙ I d · ˙ Z N Y Z
65 1 13 14 15 2 27 22 7 42 lmodsubdi φ d · ˙ X - ˙ Z = d · ˙ X - ˙ d · ˙ Z
66 1 14 13 15 lmodvscl W LMod d B X V d · ˙ X V
67 27 22 7 66 syl3anc φ d · ˙ X V
68 1 12 2 13 14 15 19 27 22 67 42 lmodsubvs φ d · ˙ X - ˙ d · ˙ Z = d · ˙ X + ˙ I d · ˙ Z
69 65 68 eqtrd φ d · ˙ X - ˙ Z = d · ˙ X + ˙ I d · ˙ Z
70 69 oveq1d φ d · ˙ X - ˙ Z + ˙ e · ˙ Y = d · ˙ X + ˙ I d · ˙ Z + ˙ e · ˙ Y
71 lmodabl W LMod W Abel
72 6 26 71 3syl φ W Abel
73 1 14 13 15 lmodvscl W LMod I d B Z V I d · ˙ Z V
74 27 60 42 73 syl3anc φ I d · ˙ Z V
75 1 14 13 15 lmodvscl W LMod e B Y V e · ˙ Y V
76 27 23 28 75 syl3anc φ e · ˙ Y V
77 1 12 72 67 74 76 abl32 φ d · ˙ X + ˙ I d · ˙ Z + ˙ e · ˙ Y = d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z
78 1 12 lmodass W LMod d · ˙ X V e · ˙ Y V I d · ˙ Z V d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z = d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z
79 27 67 76 74 78 syl13anc φ d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z = d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z
80 70 77 79 3eqtrd φ d · ˙ X - ˙ Z + ˙ e · ˙ Y = d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z
81 25 47 80 3eqtr3d φ a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z = d · ˙ X + ˙ e · ˙ Y + ˙ I d · ˙ Z
82 1 12 14 15 13 61 6 62 7 8 63 64 20 22 81 lvecindp φ a = d I a · ˙ Y + ˙ b · ˙ Z = e · ˙ Y + ˙ I d · ˙ Z
83 82 simprd φ I a · ˙ Y + ˙ b · ˙ Z = e · ˙ Y + ˙ I d · ˙ Z
84 1 12 14 15 13 3 5 6 10 11 39 21 23 60 9 83 lvecindp2 φ I a = e b = I d
85 84 simprd φ b = I d
86 82 simpld φ a = d
87 86 fveq2d φ I a = I d
88 85 87 eqtr4d φ b = I a
89 88 oveq1d φ b · ˙ Z = I a · ˙ Z
90 89 oveq2d φ I a · ˙ Y + ˙ b · ˙ Z = I a · ˙ Y + ˙ I a · ˙ Z
91 57 58 90 3eqtr4rd φ I a · ˙ Y + ˙ b · ˙ Z = inv g W a · ˙ Y + ˙ Z
92 91 oveq2d φ a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z = a · ˙ X + ˙ inv g W a · ˙ Y + ˙ Z
93 54 55 92 3eqtr4rd φ a · ˙ X + ˙ I a · ˙ Y + ˙ b · ˙ Z = a · ˙ X - ˙ Y + ˙ Z
94 47 93 eqtrd φ j = a · ˙ X - ˙ Y + ˙ Z