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 |
|
baerlem5a.p |
|- .+ = ( +g ` W ) |
13 |
10
|
eldifad |
|- ( ph -> Y e. V ) |
14 |
11
|
eldifad |
|- ( ph -> Z e. V ) |
15 |
|
eqid |
|- ( invg ` W ) = ( invg ` W ) |
16 |
1 12 15 2
|
grpsubval |
|- ( ( Y e. V /\ Z e. V ) -> ( Y .- Z ) = ( Y .+ ( ( invg ` W ) ` Z ) ) ) |
17 |
13 14 16
|
syl2anc |
|- ( ph -> ( Y .- Z ) = ( Y .+ ( ( invg ` W ) ` Z ) ) ) |
18 |
17
|
sneqd |
|- ( ph -> { ( Y .- Z ) } = { ( Y .+ ( ( invg ` W ) ` Z ) ) } ) |
19 |
18
|
fveq2d |
|- ( ph -> ( N ` { ( Y .- Z ) } ) = ( N ` { ( Y .+ ( ( invg ` W ) ` Z ) ) } ) ) |
20 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
21 |
6 20
|
syl |
|- ( ph -> W e. LMod ) |
22 |
1 15
|
lmodvnegcl |
|- ( ( W e. LMod /\ Z e. V ) -> ( ( invg ` W ) ` Z ) e. V ) |
23 |
21 14 22
|
syl2anc |
|- ( ph -> ( ( invg ` W ) ` Z ) e. V ) |
24 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
25 |
1 24 5 21 13 14
|
lspprcl |
|- ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) ) |
26 |
3 24 21 25 7 8
|
lssneln0 |
|- ( ph -> X e. ( V \ { .0. } ) ) |
27 |
1 5 6 7 13 14 8
|
lspindpi |
|- ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) ) |
28 |
27
|
simpld |
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
29 |
1 3 5 6 26 13 28
|
lspsnne1 |
|- ( ph -> -. X e. ( N ` { Y } ) ) |
30 |
9
|
necomd |
|- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) ) |
31 |
1 3 5 6 11 13 30
|
lspsnne1 |
|- ( ph -> -. Z e. ( N ` { Y } ) ) |
32 |
1 5 6 7 14 13 31 8
|
lspexchn2 |
|- ( ph -> -. Z e. ( N ` { Y , X } ) ) |
33 |
|
lmodgrp |
|- ( W e. LMod -> W e. Grp ) |
34 |
21 33
|
syl |
|- ( ph -> W e. Grp ) |
35 |
34
|
adantr |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> W e. Grp ) |
36 |
14
|
adantr |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> Z e. V ) |
37 |
1 15
|
grpinvinv |
|- ( ( W e. Grp /\ Z e. V ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) = Z ) |
38 |
35 36 37
|
syl2anc |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) = Z ) |
39 |
21
|
adantr |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> W e. LMod ) |
40 |
1 24 5 21 13 7
|
lspprcl |
|- ( ph -> ( N ` { Y , X } ) e. ( LSubSp ` W ) ) |
41 |
40
|
adantr |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( N ` { Y , X } ) e. ( LSubSp ` W ) ) |
42 |
|
simpr |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) |
43 |
24 15
|
lssvnegcl |
|- ( ( W e. LMod /\ ( N ` { Y , X } ) e. ( LSubSp ` W ) /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) e. ( N ` { Y , X } ) ) |
44 |
39 41 42 43
|
syl3anc |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Z ) ) e. ( N ` { Y , X } ) ) |
45 |
38 44
|
eqeltrrd |
|- ( ( ph /\ ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) -> Z e. ( N ` { Y , X } ) ) |
46 |
32 45
|
mtand |
|- ( ph -> -. ( ( invg ` W ) ` Z ) e. ( N ` { Y , X } ) ) |
47 |
1 5 6 23 7 13 29 46
|
lspexchn2 |
|- ( ph -> -. X e. ( N ` { Y , ( ( invg ` W ) ` Z ) } ) ) |
48 |
1 15 5
|
lspsnneg |
|- ( ( W e. LMod /\ Z e. V ) -> ( N ` { ( ( invg ` W ) ` Z ) } ) = ( N ` { Z } ) ) |
49 |
21 14 48
|
syl2anc |
|- ( ph -> ( N ` { ( ( invg ` W ) ` Z ) } ) = ( N ` { Z } ) ) |
50 |
9 49
|
neeqtrrd |
|- ( ph -> ( N ` { Y } ) =/= ( N ` { ( ( invg ` W ) ` Z ) } ) ) |
51 |
1 3 15
|
grpinvnzcl |
|- ( ( W e. Grp /\ Z e. ( V \ { .0. } ) ) -> ( ( invg ` W ) ` Z ) e. ( V \ { .0. } ) ) |
52 |
34 11 51
|
syl2anc |
|- ( ph -> ( ( invg ` W ) ` Z ) e. ( V \ { .0. } ) ) |
53 |
1 2 3 4 5 6 7 47 50 10 52 12
|
baerlem5b |
|- ( ph -> ( N ` { ( Y .+ ( ( invg ` W ) ` Z ) ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { ( ( invg ` W ) ` Z ) } ) ) i^i ( ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) .(+) ( N ` { X } ) ) ) ) |
54 |
49
|
oveq2d |
|- ( ph -> ( ( N ` { Y } ) .(+) ( N ` { ( ( invg ` W ) ` Z ) } ) ) = ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) |
55 |
17
|
eqcomd |
|- ( ph -> ( Y .+ ( ( invg ` W ) ` Z ) ) = ( Y .- Z ) ) |
56 |
55
|
oveq2d |
|- ( ph -> ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) = ( X .- ( Y .- Z ) ) ) |
57 |
56
|
sneqd |
|- ( ph -> { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } = { ( X .- ( Y .- Z ) ) } ) |
58 |
57
|
fveq2d |
|- ( ph -> ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) = ( N ` { ( X .- ( Y .- Z ) ) } ) ) |
59 |
58
|
oveq1d |
|- ( ph -> ( ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) .(+) ( N ` { X } ) ) = ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) |
60 |
54 59
|
ineq12d |
|- ( ph -> ( ( ( N ` { Y } ) .(+) ( N ` { ( ( invg ` W ) ` Z ) } ) ) i^i ( ( N ` { ( X .- ( Y .+ ( ( invg ` W ) ` Z ) ) ) } ) .(+) ( N ` { X } ) ) ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) ) |
61 |
19 53 60
|
3eqtrd |
|- ( ph -> ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) ) |