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 syl5bb
 |-  ( 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 lspsneli
 |-  ( ( ( 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 } ) ) ) )