Metamath Proof Explorer

Theorem baerlem5blem2

Description: Lemma for baerlem5b . (Contributed by NM, 13-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 baerlem5blem2 
|- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )

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 12 5 4 lspsntri 
 |-  ( ( 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 12 lmodvacl 
 |-  ( ( W e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
27 21 22 23 26 syl3anc 
 |-  ( ph -> ( Y .+ Z ) e. V )
28 1 2 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ ( Y .+ Z ) e. V ) -> ( X .- ( Y .+ Z ) ) e. V )
29 21 7 27 28 syl3anc 
 |-  ( ph -> ( X .- ( Y .+ Z ) ) e. V )
30 1 2 5 21 29 7 lspsnsub 
 |-  ( ph -> ( N ` { ( ( X .- ( Y .+ Z ) ) .- X ) } ) = ( N ` { ( X .- ( X .- ( Y .+ Z ) ) ) } ) )
31 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
32 21 31 syl 
 |-  ( ph -> W e. Abel )
33 1 2 32 7 27 ablnncan 
 |-  ( ph -> ( X .- ( X .- ( Y .+ Z ) ) ) = ( Y .+ Z ) )
34 33 sneqd 
 |-  ( ph -> { ( X .- ( X .- ( Y .+ Z ) ) ) } = { ( Y .+ Z ) } )
35 34 fveq2d 
 |-  ( ph -> ( N ` { ( X .- ( X .- ( Y .+ Z ) ) ) } ) = ( N ` { ( Y .+ Z ) } ) )
36 30 35 eqtrd 
 |-  ( ph -> ( N ` { ( ( X .- ( Y .+ Z ) ) .- X ) } ) = ( N ` { ( Y .+ Z ) } ) )
37 1 2 4 5 lspsntrim 
 |-  ( ( W e. LMod /\ ( X .- ( Y .+ Z ) ) e. V /\ X e. V ) -> ( N ` { ( ( X .- ( Y .+ Z ) ) .- X ) } ) C_ ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) )
38 21 29 7 37 syl3anc 
 |-  ( ph -> ( N ` { ( ( X .- ( Y .+ Z ) ) .- X ) } ) C_ ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) )
39 36 38 eqsstrrd 
 |-  ( ph -> ( N ` { ( Y .+ Z ) } ) C_ ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) )
40 25 39 ssind 
 |-  ( ph -> ( N ` { ( Y .+ Z ) } ) C_ ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )
41 elin 
 |-  ( j e. ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) <-> ( j e. ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) /\ j e. ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )
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 29 7 lsmspsn 
 |-  ( ph -> ( j e. ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) <-> E. d e. B E. e e. B j = ( ( d .x. ( X .- ( Y .+ Z ) ) ) .+ ( e .x. X ) ) ) )
44 42 43 anbi12d 
 |-  ( ph -> ( ( j e. ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) /\ j e. ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) <-> ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) ) )
45 41 44 syl5bb 
 |-  ( ph -> ( j e. ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) <-> ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) ) )
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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> -. 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> j = ( ( d .x. ( X .- ( Y .+ Z ) ) ) .+ ( e .x. X ) ) )
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 baerlem5blem1 
 |-  ( ( ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> j = ( ( I ` d ) .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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> W e. LMod )
61 14 lmodring 
 |-  ( W e. LMod -> R e. Ring )
62 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
63 46 21 61 62 4syl 
 |-  ( ( ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> R e. Grp )
64 15 19 grpinvcl 
 |-  ( ( R e. Grp /\ d e. B ) -> ( I ` d ) e. B )
65 63 55 64 syl2anc 
 |-  ( ( ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> ( I ` d ) e. B )
66 46 27 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> ( Y .+ Z ) e. V )
67 1 13 14 15 5 60 65 66 lspsneli 
 |-  ( ( ( 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> ( ( I ` d ) .x. ( Y .+ Z ) ) e. ( N ` { ( Y .+ Z ) } ) )
68 59 67 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> j e. ( N ` { ( Y .+ Z ) } ) )
69 68 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 .+ Z ) ) ) .+ ( e .x. X ) ) -> j e. ( N ` { ( Y .+ Z ) } ) ) ) )
70 69 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 .+ Z ) ) ) .+ ( e .x. X ) ) -> j e. ( N ` { ( Y .+ Z ) } ) ) )
71 70 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 .+ Z ) ) ) .+ ( e .x. X ) ) -> j e. ( N ` { ( Y .+ Z ) } ) ) ) ) )
72 71 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 .+ Z ) ) ) .+ ( e .x. X ) ) -> j e. ( N ` { ( Y .+ Z ) } ) ) ) )
73 72 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 .+ Z ) ) ) .+ ( e .x. X ) ) ) -> j e. ( N ` { ( Y .+ Z ) } ) ) )
74 45 73 sylbid 
 |-  ( ph -> ( j e. ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) -> j e. ( N ` { ( Y .+ Z ) } ) ) )
75 74 ssrdv 
 |-  ( ph -> ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) C_ ( N ` { ( Y .+ Z ) } ) )
76 40 75 eqssd 
 |-  ( ph -> ( N ` { ( Y .+ Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )