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 
|- .- = ( -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 )
baerlem5a.a1 
|- ( ph -> a e. B )
baerlem5a.b1 
|- ( ph -> b e. B )
baerlem5a.d1 
|- ( ph -> d e. B )
baerlem5a.e1 
|- ( ph -> e e. B )
baerlem5a.j1 
|- ( ph -> j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) )
baerlem5a.j2 
|- ( ph -> j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) )
Assertion baerlem5alem1 
|- ( ph -> j = ( a .x. ( 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 baerlem5a.a1 
 |-  ( ph -> a e. B )
21 baerlem5a.b1 
 |-  ( ph -> b e. B )
22 baerlem5a.d1 
 |-  ( ph -> d e. B )
23 baerlem5a.e1 
 |-  ( ph -> e e. B )
24 baerlem5a.j1 
 |-  ( ph -> j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) )
25 baerlem5a.j2 
 |-  ( ph -> j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) )
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 13 14 15 2 27 20 7 28 lmodsubdi 
 |-  ( ph -> ( a .x. ( X .- Y ) ) = ( ( a .x. X ) .- ( a .x. Y ) ) )
30 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ a e. B /\ X e. V ) -> ( a .x. X ) e. V )
31 27 20 7 30 syl3anc 
 |-  ( ph -> ( a .x. X ) e. V )
32 1 12 2 13 14 15 19 27 20 31 28 lmodsubvs 
 |-  ( ph -> ( ( a .x. X ) .- ( a .x. Y ) ) = ( ( a .x. X ) .+ ( ( I ` a ) .x. Y ) ) )
33 29 32 eqtrd 
 |-  ( ph -> ( a .x. ( X .- Y ) ) = ( ( a .x. X ) .+ ( ( I ` a ) .x. Y ) ) )
34 33 oveq1d 
 |-  ( ph -> ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) = ( ( ( a .x. X ) .+ ( ( I ` a ) .x. Y ) ) .+ ( b .x. Z ) ) )
35 14 lmodring 
 |-  ( W e. LMod -> R e. Ring )
36 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
37 27 35 36 3syl 
 |-  ( ph -> R e. Grp )
38 15 19 grpinvcl 
 |-  ( ( R e. Grp /\ a e. B ) -> ( I ` a ) e. B )
39 37 20 38 syl2anc 
 |-  ( ph -> ( I ` a ) e. B )
40 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ ( I ` a ) e. B /\ Y e. V ) -> ( ( I ` a ) .x. Y ) e. V )
41 27 39 28 40 syl3anc 
 |-  ( ph -> ( ( I ` a ) .x. Y ) e. V )
42 11 eldifad 
 |-  ( ph -> Z e. V )
43 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ b e. B /\ Z e. V ) -> ( b .x. Z ) e. V )
44 27 21 42 43 syl3anc 
 |-  ( ph -> ( b .x. Z ) e. V )
45 1 12 lmodass 
 |-  ( ( W e. LMod /\ ( ( a .x. X ) e. V /\ ( ( I ` a ) .x. Y ) e. V /\ ( b .x. Z ) e. V ) ) -> ( ( ( a .x. X ) .+ ( ( I ` a ) .x. Y ) ) .+ ( b .x. Z ) ) = ( ( a .x. X ) .+ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) ) )
46 27 31 41 44 45 syl13anc 
 |-  ( ph -> ( ( ( a .x. X ) .+ ( ( I ` a ) .x. Y ) ) .+ ( b .x. Z ) ) = ( ( a .x. X ) .+ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) ) )
47 24 34 46 3eqtrd 
 |-  ( ph -> j = ( ( a .x. X ) .+ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) ) )
48 1 12 lmodvacl 
 |-  ( ( W e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
49 27 28 42 48 syl3anc 
 |-  ( ph -> ( Y .+ Z ) e. V )
50 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ a e. B /\ ( Y .+ Z ) e. V ) -> ( a .x. ( Y .+ Z ) ) e. V )
51 27 20 49 50 syl3anc 
 |-  ( ph -> ( a .x. ( Y .+ Z ) ) e. V )
52 eqid 
 |-  ( invg ` W ) = ( invg ` W )
53 1 12 52 2 grpsubval 
 |-  ( ( ( a .x. X ) e. V /\ ( a .x. ( Y .+ Z ) ) e. V ) -> ( ( a .x. X ) .- ( a .x. ( Y .+ Z ) ) ) = ( ( a .x. X ) .+ ( ( invg ` W ) ` ( a .x. ( Y .+ Z ) ) ) ) )
54 31 51 53 syl2anc 
 |-  ( ph -> ( ( a .x. X ) .- ( a .x. ( Y .+ Z ) ) ) = ( ( a .x. X ) .+ ( ( invg ` W ) ` ( a .x. ( Y .+ Z ) ) ) ) )
55 1 13 14 15 2 27 20 7 49 lmodsubdi 
 |-  ( ph -> ( a .x. ( X .- ( Y .+ Z ) ) ) = ( ( a .x. X ) .- ( a .x. ( Y .+ Z ) ) ) )
56 1 12 14 13 15 lmodvsdi 
 |-  ( ( W e. LMod /\ ( ( I ` a ) e. B /\ Y e. V /\ Z e. V ) ) -> ( ( I ` a ) .x. ( Y .+ Z ) ) = ( ( ( I ` a ) .x. Y ) .+ ( ( I ` a ) .x. Z ) ) )
57 27 39 28 42 56 syl13anc 
 |-  ( ph -> ( ( I ` a ) .x. ( Y .+ Z ) ) = ( ( ( I ` a ) .x. Y ) .+ ( ( I ` a ) .x. Z ) ) )
58 1 14 13 52 15 19 27 49 20 lmodvsneg 
 |-  ( ph -> ( ( invg ` W ) ` ( a .x. ( Y .+ Z ) ) ) = ( ( I ` a ) .x. ( Y .+ Z ) ) )
59 15 19 grpinvcl 
 |-  ( ( R e. Grp /\ d e. B ) -> ( I ` d ) e. B )
60 37 22 59 syl2anc 
 |-  ( ph -> ( I ` d ) e. B )
61 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
62 1 61 5 27 28 42 lspprcl 
 |-  ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
63 1 12 13 14 15 5 27 39 21 28 42 lsppreli 
 |-  ( ph -> ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) e. ( N ` { Y , Z } ) )
64 1 12 13 14 15 5 27 23 60 28 42 lsppreli 
 |-  ( ph -> ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) e. ( N ` { Y , Z } ) )
65 1 13 14 15 2 27 22 7 42 lmodsubdi 
 |-  ( ph -> ( d .x. ( X .- Z ) ) = ( ( d .x. X ) .- ( d .x. Z ) ) )
66 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ d e. B /\ X e. V ) -> ( d .x. X ) e. V )
67 27 22 7 66 syl3anc 
 |-  ( ph -> ( d .x. X ) e. V )
68 1 12 2 13 14 15 19 27 22 67 42 lmodsubvs 
 |-  ( ph -> ( ( d .x. X ) .- ( d .x. Z ) ) = ( ( d .x. X ) .+ ( ( I ` d ) .x. Z ) ) )
69 65 68 eqtrd 
 |-  ( ph -> ( d .x. ( X .- Z ) ) = ( ( d .x. X ) .+ ( ( I ` d ) .x. Z ) ) )
70 69 oveq1d 
 |-  ( ph -> ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) = ( ( ( d .x. X ) .+ ( ( I ` d ) .x. Z ) ) .+ ( e .x. Y ) ) )
71 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
72 6 26 71 3syl 
 |-  ( ph -> W e. Abel )
73 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ ( I ` d ) e. B /\ Z e. V ) -> ( ( I ` d ) .x. Z ) e. V )
74 27 60 42 73 syl3anc 
 |-  ( ph -> ( ( I ` d ) .x. Z ) e. V )
75 1 14 13 15 lmodvscl 
 |-  ( ( W e. LMod /\ e e. B /\ Y e. V ) -> ( e .x. Y ) e. V )
76 27 23 28 75 syl3anc 
 |-  ( ph -> ( e .x. Y ) e. V )
77 1 12 72 67 74 76 abl32 
 |-  ( ph -> ( ( ( d .x. X ) .+ ( ( I ` d ) .x. Z ) ) .+ ( e .x. Y ) ) = ( ( ( d .x. X ) .+ ( e .x. Y ) ) .+ ( ( I ` d ) .x. Z ) ) )
78 1 12 lmodass 
 |-  ( ( W e. LMod /\ ( ( d .x. X ) e. V /\ ( e .x. Y ) e. V /\ ( ( I ` d ) .x. Z ) e. V ) ) -> ( ( ( d .x. X ) .+ ( e .x. Y ) ) .+ ( ( I ` d ) .x. Z ) ) = ( ( d .x. X ) .+ ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) ) )
79 27 67 76 74 78 syl13anc 
 |-  ( ph -> ( ( ( d .x. X ) .+ ( e .x. Y ) ) .+ ( ( I ` d ) .x. Z ) ) = ( ( d .x. X ) .+ ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) ) )
80 70 77 79 3eqtrd 
 |-  ( ph -> ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) = ( ( d .x. X ) .+ ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) ) )
81 25 47 80 3eqtr3d 
 |-  ( ph -> ( ( a .x. X ) .+ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) ) = ( ( d .x. X ) .+ ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) ) )
82 1 12 14 15 13 61 6 62 7 8 63 64 20 22 81 lvecindp 
 |-  ( ph -> ( a = d /\ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) = ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) ) )
83 82 simprd 
 |-  ( ph -> ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) = ( ( e .x. Y ) .+ ( ( I ` d ) .x. Z ) ) )
84 1 12 14 15 13 3 5 6 10 11 39 21 23 60 9 83 lvecindp2 
 |-  ( ph -> ( ( I ` a ) = e /\ b = ( I ` d ) ) )
85 84 simprd 
 |-  ( ph -> b = ( I ` d ) )
86 82 simpld 
 |-  ( ph -> a = d )
87 86 fveq2d 
 |-  ( ph -> ( I ` a ) = ( I ` d ) )
88 85 87 eqtr4d 
 |-  ( ph -> b = ( I ` a ) )
89 88 oveq1d 
 |-  ( ph -> ( b .x. Z ) = ( ( I ` a ) .x. Z ) )
90 89 oveq2d 
 |-  ( ph -> ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) = ( ( ( I ` a ) .x. Y ) .+ ( ( I ` a ) .x. Z ) ) )
91 57 58 90 3eqtr4rd 
 |-  ( ph -> ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) = ( ( invg ` W ) ` ( a .x. ( Y .+ Z ) ) ) )
92 91 oveq2d 
 |-  ( ph -> ( ( a .x. X ) .+ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) ) = ( ( a .x. X ) .+ ( ( invg ` W ) ` ( a .x. ( Y .+ Z ) ) ) ) )
93 54 55 92 3eqtr4rd 
 |-  ( ph -> ( ( a .x. X ) .+ ( ( ( I ` a ) .x. Y ) .+ ( b .x. Z ) ) ) = ( a .x. ( X .- ( Y .+ Z ) ) ) )
94 47 93 eqtrd 
 |-  ( ph -> j = ( a .x. ( X .- ( Y .+ Z ) ) ) )