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 } ) ) ) ) |