Metamath Proof Explorer

Theorem baerlem3lem2

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