Metamath Proof Explorer

Theorem baerlem3lem1

Description: Lemma for baerlem3 . (Contributed by NM, 9-Apr-2015)

Ref Expression
Hypotheses baerlem3.v 
|- V = ( Base ` W )
baerlem3.m 
|- .- = ( -g ` W )
baerlem3.o 
|- .0. = ( 0g ` W )
baerlem3.s 
|- .(+) = ( LSSum ` W )
baerlem3.n 
|- N = ( LSpan ` W )
baerlem3.w 
|- ( ph -> W e. LVec )
baerlem3.x 
|- ( ph -> X e. V )
baerlem3.c 
|- ( ph -> -. X e. ( N ` { Y , Z } ) )
baerlem3.d 
|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
baerlem3.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
baerlem3.z 
|- ( ph -> Z e. ( V \ { .0. } ) )
baerlem3.p 
|- .+ = ( +g ` W )
baerlem3.t 
|- .x. = ( .s ` W )
baerlem3.r 
|- R = ( Scalar ` W )
baerlem3.b 
|- B = ( Base ` R )
baerlem3.a 
|- .+^ = ( +g ` R )
baerlem3.l 
|- L = ( -g ` R )
baerlem3.q 
|- Q = ( 0g ` R )
baerlem3.i 
|- I = ( invg ` R )
baerlem3.a1 
|- ( ph -> a e. B )
baerlem3.b1 
|- ( ph -> b e. B )
baerlem3.d1 
|- ( ph -> d e. B )
baerlem3.e1 
|- ( ph -> e e. B )
baerlem3.j1 
|- ( ph -> j = ( ( a .x. Y ) .+ ( b .x. Z ) ) )
baerlem3.j2 
|- ( ph -> j = ( ( d .x. ( X .- Y ) ) .+ ( e .x. ( X .- Z ) ) ) )
Assertion baerlem3lem1 
|- ( ph -> j = ( a .x. ( Y .- Z ) ) )

Proof

Step Hyp Ref Expression
1 baerlem3.v 
 |-  V = ( Base ` W )
2 baerlem3.m 
 |-  .- = ( -g ` W )
3 baerlem3.o 
 |-  .0. = ( 0g ` W )
4 baerlem3.s 
 |-  .(+) = ( LSSum ` W )
5 baerlem3.n 
 |-  N = ( LSpan ` W )
6 baerlem3.w 
 |-  ( ph -> W e. LVec )
7 baerlem3.x 
 |-  ( ph -> X e. V )
8 baerlem3.c 
 |-  ( ph -> -. X e. ( N ` { Y , Z } ) )
9 baerlem3.d 
 |-  ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
10 baerlem3.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
11 baerlem3.z 
 |-  ( ph -> Z e. ( V \ { .0. } ) )
12 baerlem3.p 
 |-  .+ = ( +g ` W )
13 baerlem3.t 
 |-  .x. = ( .s ` W )
14 baerlem3.r 
 |-  R = ( Scalar ` W )
15 baerlem3.b 
 |-  B = ( Base ` R )
16 baerlem3.a 
 |-  .+^ = ( +g ` R )
17 baerlem3.l 
 |-  L = ( -g ` R )
18 baerlem3.q 
 |-  Q = ( 0g ` R )
19 baerlem3.i 
 |-  I = ( invg ` R )
20 baerlem3.a1 
 |-  ( ph -> a e. B )
21 baerlem3.b1 
 |-  ( ph -> b e. B )
22 baerlem3.d1 
 |-  ( ph -> d e. B )
23 baerlem3.e1 
 |-  ( ph -> e e. B )
24 baerlem3.j1 
 |-  ( ph -> j = ( ( a .x. Y ) .+ ( b .x. Z ) ) )
25 baerlem3.j2 
 |-  ( ph -> j = ( ( d .x. ( X .- Y ) ) .+ ( e .x. ( X .- Z ) ) ) )
26 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
27 6 26 syl 
 |-  ( ph -> W e. LMod )
28 10 eldifad 
 |-  ( ph -> Y e. V )
29 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ a e. B /\ Y e. V ) -> ( a .x. Y ) e. V )
30 27 20 28 29 syl3anc 
 |-  ( ph -> ( a .x. Y ) e. V )
31 11 eldifad 
 |-  ( ph -> Z e. V )
32 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ a e. B /\ Z e. V ) -> ( a .x. Z ) e. V )
33 27 20 31 32 syl3anc 
 |-  ( ph -> ( a .x. Z ) e. V )
34 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
35 1 12 2 14 13 19 34 lmodvsubval2 
 |-  ( ( W e. LMod /\ ( a .x. Y ) e. V /\ ( a .x. Z ) e. V ) -> ( ( a .x. Y ) .- ( a .x. Z ) ) = ( ( a .x. Y ) .+ ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) ) )
36 27 30 33 35 syl3anc 
 |-  ( ph -> ( ( a .x. Y ) .- ( a .x. Z ) ) = ( ( a .x. Y ) .+ ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) ) )
37 1 13 14 15 2 27 20 28 31 lmodsubdi 
 |-  ( ph -> ( a .x. ( Y .- Z ) ) = ( ( a .x. Y ) .- ( a .x. Z ) ) )
38 14 lmodring 
 |-  ( W e. LMod -> R e. Ring )
39 27 38 syl 
 |-  ( ph -> R e. Ring )
40 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
41 39 40 syl 
 |-  ( ph -> R e. Grp )
42 14 15 34 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` R ) e. B )
43 27 42 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
44 15 19 grpinvcl 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. B ) -> ( I ` ( 1r ` R ) ) e. B )
45 41 43 44 syl2anc 
 |-  ( ph -> ( I ` ( 1r ` R ) ) e. B )
46 eqid 
 |-  ( .r ` R ) = ( .r ` R )
47 1 14 13 15 46 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( I ` ( 1r ` R ) ) e. B /\ a e. B /\ Z e. V ) ) -> ( ( ( I ` ( 1r ` R ) ) ( .r ` R ) a ) .x. Z ) = ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) )
48 27 45 20 31 47 syl13anc 
 |-  ( ph -> ( ( ( I ` ( 1r ` R ) ) ( .r ` R ) a ) .x. Z ) = ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) )
49 15 46 34 19 39 20 ringnegl 
 |-  ( ph -> ( ( I ` ( 1r ` R ) ) ( .r ` R ) a ) = ( I ` a ) )
50 ringabl 
 |-  ( R e. Ring -> R e. Abel )
51 39 50 syl 
 |-  ( ph -> R e. Abel )
52 15 16 19 ablinvadd 
 |-  ( ( R e. Abel /\ d e. B /\ e e. B ) -> ( I ` ( d .+^ e ) ) = ( ( I ` d ) .+^ ( I ` e ) ) )
53 51 22 23 52 syl3anc 
 |-  ( ph -> ( I ` ( d .+^ e ) ) = ( ( I ` d ) .+^ ( I ` e ) ) )
54 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
55 1 54 5 27 28 31 lspprcl 
 |-  ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
56 1 12 13 14 15 5 27 20 21 28 31 lsppreli 
 |-  ( ph -> ( ( a .x. Y ) .+ ( b .x. Z ) ) e. ( N ` { Y , Z } ) )
57 1 12 13 14 15 5 27 22 23 28 31 lsppreli 
 |-  ( ph -> ( ( d .x. Y ) .+ ( e .x. Z ) ) e. ( N ` { Y , Z } ) )
58 eqid 
 |-  ( invg ` W ) = ( invg ` W )
59 54 58 lssvnegcl 
 |-  ( ( W e. LMod /\ ( N ` { Y , Z } ) e. ( LSubSp ` W ) /\ ( ( d .x. Y ) .+ ( e .x. Z ) ) e. ( N ` { Y , Z } ) ) -> ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) e. ( N ` { Y , Z } ) )
60 27 55 57 59 syl3anc 
 |-  ( ph -> ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) e. ( N ` { Y , Z } ) )
61 15 18 ring0cl 
 |-  ( R e. Ring -> Q e. B )
62 39 61 syl 
 |-  ( ph -> Q e. B )
63 15 16 ringacl 
 |-  ( ( R e. Ring /\ d e. B /\ e e. B ) -> ( d .+^ e ) e. B )
64 39 22 23 63 syl3anc 
 |-  ( ph -> ( d .+^ e ) e. B )
65 1 14 13 18 3 lmod0vs 
 |-  ( ( W e. LMod /\ X e. V ) -> ( Q .x. X ) = .0. )
66 27 7 65 syl2anc 
 |-  ( ph -> ( Q .x. X ) = .0. )
67 66 oveq1d 
 |-  ( ph -> ( ( Q .x. X ) .+ ( ( a .x. Y ) .+ ( b .x. Z ) ) ) = ( .0. .+ ( ( a .x. Y ) .+ ( b .x. Z ) ) ) )
68 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
69 27 68 syl 
 |-  ( ph -> W e. Grp )
70 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ b e. B /\ Z e. V ) -> ( b .x. Z ) e. V )
71 27 21 31 70 syl3anc 
 |-  ( ph -> ( b .x. Z ) e. V )
72 1 12 lmodvacl 
 |-  ( ( W e. LMod /\ ( a .x. Y ) e. V /\ ( b .x. Z ) e. V ) -> ( ( a .x. Y ) .+ ( b .x. Z ) ) e. V )
73 27 30 71 72 syl3anc 
 |-  ( ph -> ( ( a .x. Y ) .+ ( b .x. Z ) ) e. V )
74 1 12 3 grplid 
 |-  ( ( W e. Grp /\ ( ( a .x. Y ) .+ ( b .x. Z ) ) e. V ) -> ( .0. .+ ( ( a .x. Y ) .+ ( b .x. Z ) ) ) = ( ( a .x. Y ) .+ ( b .x. Z ) ) )
75 69 73 74 syl2anc 
 |-  ( ph -> ( .0. .+ ( ( a .x. Y ) .+ ( b .x. Z ) ) ) = ( ( a .x. Y ) .+ ( b .x. Z ) ) )
76 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
77 27 76 syl 
 |-  ( ph -> W e. Abel )
78 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ d e. B /\ X e. V ) -> ( d .x. X ) e. V )
79 27 22 7 78 syl3anc 
 |-  ( ph -> ( d .x. X ) e. V )
80 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ e e. B /\ X e. V ) -> ( e .x. X ) e. V )
81 27 23 7 80 syl3anc 
 |-  ( ph -> ( e .x. X ) e. V )
82 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ d e. B /\ Y e. V ) -> ( d .x. Y ) e. V )
83 27 22 28 82 syl3anc 
 |-  ( ph -> ( d .x. Y ) e. V )
84 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ e e. B /\ Z e. V ) -> ( e .x. Z ) e. V )
85 27 23 31 84 syl3anc 
 |-  ( ph -> ( e .x. Z ) e. V )
86 1 12 2 ablsub4 
 |-  ( ( W e. Abel /\ ( ( d .x. X ) e. V /\ ( e .x. X ) e. V ) /\ ( ( d .x. Y ) e. V /\ ( e .x. Z ) e. V ) ) -> ( ( ( d .x. X ) .+ ( e .x. X ) ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) = ( ( ( d .x. X ) .- ( d .x. Y ) ) .+ ( ( e .x. X ) .- ( e .x. Z ) ) ) )
87 77 79 81 83 85 86 syl122anc 
 |-  ( ph -> ( ( ( d .x. X ) .+ ( e .x. X ) ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) = ( ( ( d .x. X ) .- ( d .x. Y ) ) .+ ( ( e .x. X ) .- ( e .x. Z ) ) ) )
88 1 12 14 13 15 16 lmodvsdir 
 |-  ( ( W e. LMod /\ ( d e. B /\ e e. B /\ X e. V ) ) -> ( ( d .+^ e ) .x. X ) = ( ( d .x. X ) .+ ( e .x. X ) ) )
89 27 22 23 7 88 syl13anc 
 |-  ( ph -> ( ( d .+^ e ) .x. X ) = ( ( d .x. X ) .+ ( e .x. X ) ) )
90 89 oveq1d 
 |-  ( ph -> ( ( ( d .+^ e ) .x. X ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) = ( ( ( d .x. X ) .+ ( e .x. X ) ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) )
91 1 13 14 15 2 27 22 7 28 lmodsubdi 
 |-  ( ph -> ( d .x. ( X .- Y ) ) = ( ( d .x. X ) .- ( d .x. Y ) ) )
92 1 13 14 15 2 27 23 7 31 lmodsubdi 
 |-  ( ph -> ( e .x. ( X .- Z ) ) = ( ( e .x. X ) .- ( e .x. Z ) ) )
93 91 92 oveq12d 
 |-  ( ph -> ( ( d .x. ( X .- Y ) ) .+ ( e .x. ( X .- Z ) ) ) = ( ( ( d .x. X ) .- ( d .x. Y ) ) .+ ( ( e .x. X ) .- ( e .x. Z ) ) ) )
94 25 93 eqtrd 
 |-  ( ph -> j = ( ( ( d .x. X ) .- ( d .x. Y ) ) .+ ( ( e .x. X ) .- ( e .x. Z ) ) ) )
95 87 90 94 3eqtr4rd 
 |-  ( ph -> j = ( ( ( d .+^ e ) .x. X ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) )
96 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ ( d .+^ e ) e. B /\ X e. V ) -> ( ( d .+^ e ) .x. X ) e. V )
97 27 64 7 96 syl3anc 
 |-  ( ph -> ( ( d .+^ e ) .x. X ) e. V )
98 1 12 lmodvacl 
 |-  ( ( W e. LMod /\ ( d .x. Y ) e. V /\ ( e .x. Z ) e. V ) -> ( ( d .x. Y ) .+ ( e .x. Z ) ) e. V )
99 27 83 85 98 syl3anc 
 |-  ( ph -> ( ( d .x. Y ) .+ ( e .x. Z ) ) e. V )
100 1 12 58 2 grpsubval 
 |-  ( ( ( ( d .+^ e ) .x. X ) e. V /\ ( ( d .x. Y ) .+ ( e .x. Z ) ) e. V ) -> ( ( ( d .+^ e ) .x. X ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) = ( ( ( d .+^ e ) .x. X ) .+ ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) ) )
101 97 99 100 syl2anc 
 |-  ( ph -> ( ( ( d .+^ e ) .x. X ) .- ( ( d .x. Y ) .+ ( e .x. Z ) ) ) = ( ( ( d .+^ e ) .x. X ) .+ ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) ) )
102 95 24 101 3eqtr3d 
 |-  ( ph -> ( ( a .x. Y ) .+ ( b .x. Z ) ) = ( ( ( d .+^ e ) .x. X ) .+ ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) ) )
103 67 75 102 3eqtrd 
 |-  ( ph -> ( ( Q .x. X ) .+ ( ( a .x. Y ) .+ ( b .x. Z ) ) ) = ( ( ( d .+^ e ) .x. X ) .+ ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) ) )
104 1 12 14 15 13 54 6 55 7 8 56 60 62 64 103 lvecindp 
 |-  ( ph -> ( Q = ( d .+^ e ) /\ ( ( a .x. Y ) .+ ( b .x. Z ) ) = ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) ) )
105 104 simpld 
 |-  ( ph -> Q = ( d .+^ e ) )
106 105 fveq2d 
 |-  ( ph -> ( I ` Q ) = ( I ` ( d .+^ e ) ) )
107 15 19 grpinvcl 
 |-  ( ( R e. Grp /\ d e. B ) -> ( I ` d ) e. B )
108 41 22 107 syl2anc 
 |-  ( ph -> ( I ` d ) e. B )
109 15 19 grpinvcl 
 |-  ( ( R e. Grp /\ e e. B ) -> ( I ` e ) e. B )
110 41 23 109 syl2anc 
 |-  ( ph -> ( I ` e ) e. B )
111 104 simprd 
 |-  ( ph -> ( ( a .x. Y ) .+ ( b .x. Z ) ) = ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) )
112 1 12 13 58 14 15 19 27 22 23 28 31 lmodnegadd 
 |-  ( ph -> ( ( invg ` W ) ` ( ( d .x. Y ) .+ ( e .x. Z ) ) ) = ( ( ( I ` d ) .x. Y ) .+ ( ( I ` e ) .x. Z ) ) )
113 111 112 eqtrd 
 |-  ( ph -> ( ( a .x. Y ) .+ ( b .x. Z ) ) = ( ( ( I ` d ) .x. Y ) .+ ( ( I ` e ) .x. Z ) ) )
114 1 12 14 15 13 3 5 6 10 11 20 21 108 110 9 113 lvecindp2 
 |-  ( ph -> ( a = ( I ` d ) /\ b = ( I ` e ) ) )
115 oveq12 
 |-  ( ( a = ( I ` d ) /\ b = ( I ` e ) ) -> ( a .+^ b ) = ( ( I ` d ) .+^ ( I ` e ) ) )
116 114 115 syl 
 |-  ( ph -> ( a .+^ b ) = ( ( I ` d ) .+^ ( I ` e ) ) )
117 53 106 116 3eqtr4rd 
 |-  ( ph -> ( a .+^ b ) = ( I ` Q ) )
118 18 19 grpinvid 
 |-  ( R e. Grp -> ( I ` Q ) = Q )
119 41 118 syl 
 |-  ( ph -> ( I ` Q ) = Q )
120 117 119 eqtrd 
 |-  ( ph -> ( a .+^ b ) = Q )
121 15 16 18 19 grpinvid1 
 |-  ( ( R e. Grp /\ a e. B /\ b e. B ) -> ( ( I ` a ) = b <-> ( a .+^ b ) = Q ) )
122 41 20 21 121 syl3anc 
 |-  ( ph -> ( ( I ` a ) = b <-> ( a .+^ b ) = Q ) )
123 120 122 mpbird 
 |-  ( ph -> ( I ` a ) = b )
124 49 123 eqtrd 
 |-  ( ph -> ( ( I ` ( 1r ` R ) ) ( .r ` R ) a ) = b )
125 124 oveq1d 
 |-  ( ph -> ( ( ( I ` ( 1r ` R ) ) ( .r ` R ) a ) .x. Z ) = ( b .x. Z ) )
126 48 125 eqtr3d 
 |-  ( ph -> ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) = ( b .x. Z ) )
127 126 oveq2d 
 |-  ( ph -> ( ( a .x. Y ) .+ ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) ) = ( ( a .x. Y ) .+ ( b .x. Z ) ) )
128 24 127 eqtr4d 
 |-  ( ph -> j = ( ( a .x. Y ) .+ ( ( I ` ( 1r ` R ) ) .x. ( a .x. Z ) ) ) )
129 36 37 128 3eqtr4rd 
 |-  ( ph -> j = ( a .x. ( Y .- Z ) ) )