Metamath Proof Explorer

Theorem baerlem5blem1

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