Metamath Proof Explorer

Theorem baerlem5alem2

Description: Lemma for baerlem5a . (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 )
Assertion baerlem5alem2 
|- ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )

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 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
21 6 20 syl 
 |-  ( ph -> W e. LMod )
22 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
23 21 22 syl 
 |-  ( ph -> W e. Abel )
24 10 eldifad 
 |-  ( ph -> Y e. V )
25 11 eldifad 
 |-  ( ph -> Z e. V )
26 1 12 2 23 7 24 25 ablsubsub4 
 |-  ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y .+ Z ) ) )
27 26 sneqd 
 |-  ( ph -> { ( ( X .- Y ) .- Z ) } = { ( X .- ( Y .+ Z ) ) } )
28 27 fveq2d 
 |-  ( ph -> ( N ` { ( ( X .- Y ) .- Z ) } ) = ( N ` { ( X .- ( Y .+ Z ) ) } ) )
29 1 2 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V )
30 21 7 24 29 syl3anc 
 |-  ( ph -> ( X .- Y ) e. V )
31 1 2 4 5 lspsntrim 
 |-  ( ( W e. LMod /\ ( X .- Y ) e. V /\ Z e. V ) -> ( N ` { ( ( X .- Y ) .- Z ) } ) C_ ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) )
32 21 30 25 31 syl3anc 
 |-  ( ph -> ( N ` { ( ( X .- Y ) .- Z ) } ) C_ ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) )
33 28 32 eqsstrrd 
 |-  ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) C_ ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) )
34 1 2 23 7 25 24 ablsub32 
 |-  ( ph -> ( ( X .- Z ) .- Y ) = ( ( X .- Y ) .- Z ) )
35 34 26 eqtrd 
 |-  ( ph -> ( ( X .- Z ) .- Y ) = ( X .- ( Y .+ Z ) ) )
36 35 sneqd 
 |-  ( ph -> { ( ( X .- Z ) .- Y ) } = { ( X .- ( Y .+ Z ) ) } )
37 36 fveq2d 
 |-  ( ph -> ( N ` { ( ( X .- Z ) .- Y ) } ) = ( N ` { ( X .- ( Y .+ Z ) ) } ) )
38 1 2 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ Z e. V ) -> ( X .- Z ) e. V )
39 21 7 25 38 syl3anc 
 |-  ( ph -> ( X .- Z ) e. V )
40 1 2 4 5 lspsntrim 
 |-  ( ( W e. LMod /\ ( X .- Z ) e. V /\ Y e. V ) -> ( N ` { ( ( X .- Z ) .- Y ) } ) C_ ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) )
41 21 39 24 40 syl3anc 
 |-  ( ph -> ( N ` { ( ( X .- Z ) .- Y ) } ) C_ ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) )
42 37 41 eqsstrrd 
 |-  ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) C_ ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) )
43 33 42 ssind 
 |-  ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) C_ ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )
44 elin 
 |-  ( j e. ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) <-> ( j e. ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) /\ j e. ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )
45 1 12 14 15 13 4 5 21 30 25 lsmspsn 
 |-  ( ph -> ( j e. ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) <-> E. a e. B E. b e. B j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) )
46 1 12 14 15 13 4 5 21 39 24 lsmspsn 
 |-  ( ph -> ( j e. ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) <-> E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) )
47 45 46 anbi12d 
 |-  ( ph -> ( ( j e. ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) /\ j e. ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) <-> ( E. a e. B E. b e. B j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) /\ E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) ) )
48 44 47 bitrid 
 |-  ( ph -> ( j e. ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) <-> ( E. a e. B E. b e. B j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) /\ E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) ) )
49 simp11 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> ph )
50 49 6 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> W e. LVec )
51 49 7 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> X e. V )
52 49 8 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> -. X e. ( N ` { Y , Z } ) )
53 49 9 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> ( N ` { Y } ) =/= ( N ` { Z } ) )
54 49 10 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> Y e. ( V \ { .0. } ) )
55 49 11 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> Z e. ( V \ { .0. } ) )
56 simp12l 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> a e. B )
57 simp12r 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> b e. B )
58 simp2l 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> d e. B )
59 simp2r 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> e e. B )
60 simp13 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) )
61 simp3 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) )
62 1 2 3 4 5 50 51 52 53 54 55 12 13 14 15 16 17 18 19 56 57 58 59 60 61 baerlem5alem1 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> j = ( a .x. ( X .- ( Y .+ Z ) ) ) )
63 49 21 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> W e. LMod )
64 1 12 lmodvacl 
 |-  ( ( W e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
65 21 24 25 64 syl3anc 
 |-  ( ph -> ( Y .+ Z ) e. V )
66 1 2 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ ( Y .+ Z ) e. V ) -> ( X .- ( Y .+ Z ) ) e. V )
67 21 7 65 66 syl3anc 
 |-  ( ph -> ( X .- ( Y .+ Z ) ) e. V )
68 49 67 syl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> ( X .- ( Y .+ Z ) ) e. V )
69 1 13 14 15 5 63 56 68 ellspsni 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> ( a .x. ( X .- ( Y .+ Z ) ) ) e. ( N ` { ( X .- ( Y .+ Z ) ) } ) )
70 62 69 eqeltrd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) /\ ( d e. B /\ e e. B ) /\ j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) )
71 70 3exp 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) -> ( ( d e. B /\ e e. B ) -> ( j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) ) ) )
72 71 rexlimdvv 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) ) -> ( E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) ) )
73 72 3exp 
 |-  ( ph -> ( ( a e. B /\ b e. B ) -> ( j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) -> ( E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) ) ) ) )
74 73 rexlimdvv 
 |-  ( ph -> ( E. a e. B E. b e. B j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) -> ( E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) ) ) )
75 74 impd 
 |-  ( ph -> ( ( E. a e. B E. b e. B j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) /\ E. d e. B E. e e. B j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) ) )
76 48 75 sylbid 
 |-  ( ph -> ( j e. ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) -> j e. ( N ` { ( X .- ( Y .+ Z ) ) } ) ) )
77 76 ssrdv 
 |-  ( ph -> ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) C_ ( N ` { ( X .- ( Y .+ Z ) ) } ) )
78 43 77 eqssd 
 |-  ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )