This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lindsunlem

Description: Lemma for lindsun . (Contributed by Thierry Arnoux, 9-May-2023)

Ref Expression
Hypotheses lindsun.n 
|- N = ( LSpan ` W )
lindsun.0 
|- .0. = ( 0g ` W )
lindsun.w 
|- ( ph -> W e. LVec )
lindsun.u 
|- ( ph -> U e. ( LIndS ` W ) )
lindsun.v 
|- ( ph -> V e. ( LIndS ` W ) )
lindsun.2 
|- ( ph -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
lindsunlem.o 
|- O = ( 0g ` ( Scalar ` W ) )
lindsunlem.f 
|- F = ( Base ` ( Scalar ` W ) )
lindsunlem.c 
|- ( ph -> C e. U )
lindsunlem.k 
|- ( ph -> K e. ( F \ { O } ) )
lindsunlem.1 
|- ( ph -> ( K ( .s ` W ) C ) e. ( N ` ( ( U u. V ) \ { C } ) ) )
Assertion lindsunlem 
|- ( ph -> F. )

Proof

Step Hyp Ref Expression
1 lindsun.n 
 |-  N = ( LSpan ` W )
2 lindsun.0 
 |-  .0. = ( 0g ` W )
3 lindsun.w 
 |-  ( ph -> W e. LVec )
4 lindsun.u 
 |-  ( ph -> U e. ( LIndS ` W ) )
5 lindsun.v 
 |-  ( ph -> V e. ( LIndS ` W ) )
6 lindsun.2 
 |-  ( ph -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
7 lindsunlem.o 
 |-  O = ( 0g ` ( Scalar ` W ) )
8 lindsunlem.f 
 |-  F = ( Base ` ( Scalar ` W ) )
9 lindsunlem.c 
 |-  ( ph -> C e. U )
10 lindsunlem.k 
 |-  ( ph -> K e. ( F \ { O } ) )
11 lindsunlem.1 
 |-  ( ph -> ( K ( .s ` W ) C ) e. ( N ` ( ( U u. V ) \ { C } ) ) )
12 simpr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) )
13 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
14 3 13 syl 
 |-  ( ph -> W e. LMod )
15 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
16 14 15 syl 
 |-  ( ph -> W e. Grp )
17 16 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> W e. Grp )
18 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
19 14 18 syl 
 |-  ( ph -> W e. Abel )
20 19 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> W e. Abel )
21 eqid 
 |-  ( Base ` W ) = ( Base ` W )
22 21 linds1 
 |-  ( U e. ( LIndS ` W ) -> U C_ ( Base ` W ) )
23 4 22 syl 
 |-  ( ph -> U C_ ( Base ` W ) )
24 21 1 lspssv 
 |-  ( ( W e. LMod /\ U C_ ( Base ` W ) ) -> ( N ` U ) C_ ( Base ` W ) )
25 14 23 24 syl2anc 
 |-  ( ph -> ( N ` U ) C_ ( Base ` W ) )
26 25 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( N ` U ) C_ ( Base ` W ) )
27 difssd 
 |-  ( ph -> ( U \ { C } ) C_ U )
28 21 1 lspss 
 |-  ( ( W e. LMod /\ U C_ ( Base ` W ) /\ ( U \ { C } ) C_ U ) -> ( N ` ( U \ { C } ) ) C_ ( N ` U ) )
29 14 23 27 28 syl3anc 
 |-  ( ph -> ( N ` ( U \ { C } ) ) C_ ( N ` U ) )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( N ` ( U \ { C } ) ) C_ ( N ` U ) )
31 simpllr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> x e. ( N ` ( U \ { C } ) ) )
32 30 31 sseldd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> x e. ( N ` U ) )
33 26 32 sseldd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> x e. ( Base ` W ) )
34 21 linds1 
 |-  ( V e. ( LIndS ` W ) -> V C_ ( Base ` W ) )
35 5 34 syl 
 |-  ( ph -> V C_ ( Base ` W ) )
36 21 1 lspssv 
 |-  ( ( W e. LMod /\ V C_ ( Base ` W ) ) -> ( N ` V ) C_ ( Base ` W ) )
37 14 35 36 syl2anc 
 |-  ( ph -> ( N ` V ) C_ ( Base ` W ) )
38 37 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( N ` V ) C_ ( Base ` W ) )
39 simplr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> y e. ( N ` V ) )
40 38 39 sseldd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> y e. ( Base ` W ) )
41 eqid 
 |-  ( +g ` W ) = ( +g ` W )
42 21 41 ablcom 
 |-  ( ( W e. Abel /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ( +g ` W ) y ) = ( y ( +g ` W ) x ) )
43 20 33 40 42 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( x ( +g ` W ) y ) = ( y ( +g ` W ) x ) )
44 12 43 eqtr2d 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( y ( +g ` W ) x ) = ( K ( .s ` W ) C ) )
45 10 eldifad 
 |-  ( ph -> K e. F )
46 23 9 sseldd 
 |-  ( ph -> C e. ( Base ` W ) )
47 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
48 eqid 
 |-  ( .s ` W ) = ( .s ` W )
49 21 47 48 8 lmodvscl 
 |-  ( ( W e. LMod /\ K e. F /\ C e. ( Base ` W ) ) -> ( K ( .s ` W ) C ) e. ( Base ` W ) )
50 14 45 46 49 syl3anc 
 |-  ( ph -> ( K ( .s ` W ) C ) e. ( Base ` W ) )
51 50 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( K ( .s ` W ) C ) e. ( Base ` W ) )
52 eqid 
 |-  ( -g ` W ) = ( -g ` W )
53 21 41 52 grpsubadd 
 |-  ( ( W e. Grp /\ ( ( K ( .s ` W ) C ) e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( ( K ( .s ` W ) C ) ( -g ` W ) x ) = y <-> ( y ( +g ` W ) x ) = ( K ( .s ` W ) C ) ) )
54 53 biimpar 
 |-  ( ( ( W e. Grp /\ ( ( K ( .s ` W ) C ) e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( y ( +g ` W ) x ) = ( K ( .s ` W ) C ) ) -> ( ( K ( .s ` W ) C ) ( -g ` W ) x ) = y )
55 54 an32s 
 |-  ( ( ( W e. Grp /\ ( y ( +g ` W ) x ) = ( K ( .s ` W ) C ) ) /\ ( ( K ( .s ` W ) C ) e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( K ( .s ` W ) C ) ( -g ` W ) x ) = y )
56 17 44 51 33 40 55 syl23anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( ( K ( .s ` W ) C ) ( -g ` W ) x ) = y )
57 14 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> W e. LMod )
58 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
59 21 58 1 lspcl 
 |-  ( ( W e. LMod /\ U C_ ( Base ` W ) ) -> ( N ` U ) e. ( LSubSp ` W ) )
60 14 23 59 syl2anc 
 |-  ( ph -> ( N ` U ) e. ( LSubSp ` W ) )
61 60 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( N ` U ) e. ( LSubSp ` W ) )
62 45 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> K e. F )
63 21 1 lspssid 
 |-  ( ( W e. LMod /\ U C_ ( Base ` W ) ) -> U C_ ( N ` U ) )
64 14 23 63 syl2anc 
 |-  ( ph -> U C_ ( N ` U ) )
65 64 9 sseldd 
 |-  ( ph -> C e. ( N ` U ) )
66 65 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> C e. ( N ` U ) )
67 47 48 8 58 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` U ) e. ( LSubSp ` W ) ) /\ ( K e. F /\ C e. ( N ` U ) ) ) -> ( K ( .s ` W ) C ) e. ( N ` U ) )
68 57 61 62 66 67 syl22anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( K ( .s ` W ) C ) e. ( N ` U ) )
69 52 58 lssvsubcl 
 |-  ( ( ( W e. LMod /\ ( N ` U ) e. ( LSubSp ` W ) ) /\ ( ( K ( .s ` W ) C ) e. ( N ` U ) /\ x e. ( N ` U ) ) ) -> ( ( K ( .s ` W ) C ) ( -g ` W ) x ) e. ( N ` U ) )
70 57 61 68 32 69 syl22anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( ( K ( .s ` W ) C ) ( -g ` W ) x ) e. ( N ` U ) )
71 56 70 eqeltrrd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> y e. ( N ` U ) )
72 71 39 elind 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> y e. ( ( N ` U ) i^i ( N ` V ) ) )
73 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
74 72 73 eleqtrd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> y e. { .0. } )
75 elsni 
 |-  ( y e. { .0. } -> y = .0. )
76 74 75 syl 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> y = .0. )
77 76 oveq2d 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( x ( +g ` W ) y ) = ( x ( +g ` W ) .0. ) )
78 21 41 2 grprid 
 |-  ( ( W e. Grp /\ x e. ( Base ` W ) ) -> ( x ( +g ` W ) .0. ) = x )
79 17 33 78 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( x ( +g ` W ) .0. ) = x )
80 12 77 79 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( K ( .s ` W ) C ) = x )
81 80 31 eqeltrd 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> ( K ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) )
82 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> C e. U )
83 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> K e. ( F \ { O } ) )
84 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> W e. LVec )
85 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> U e. ( LIndS ` W ) )
86 21 48 1 47 8 7 islinds2 
 |-  ( W e. LVec -> ( U e. ( LIndS ` W ) <-> ( U C_ ( Base ` W ) /\ A. c e. U A. k e. ( F \ { O } ) -. ( k ( .s ` W ) c ) e. ( N ` ( U \ { c } ) ) ) ) )
87 86 simplbda 
 |-  ( ( W e. LVec /\ U e. ( LIndS ` W ) ) -> A. c e. U A. k e. ( F \ { O } ) -. ( k ( .s ` W ) c ) e. ( N ` ( U \ { c } ) ) )
88 84 85 87 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> A. c e. U A. k e. ( F \ { O } ) -. ( k ( .s ` W ) c ) e. ( N ` ( U \ { c } ) ) )
89 oveq2 
 |-  ( c = C -> ( k ( .s ` W ) c ) = ( k ( .s ` W ) C ) )
90 sneq 
 |-  ( c = C -> { c } = { C } )
91 90 difeq2d 
 |-  ( c = C -> ( U \ { c } ) = ( U \ { C } ) )
92 91 fveq2d 
 |-  ( c = C -> ( N ` ( U \ { c } ) ) = ( N ` ( U \ { C } ) ) )
93 89 92 eleq12d 
 |-  ( c = C -> ( ( k ( .s ` W ) c ) e. ( N ` ( U \ { c } ) ) <-> ( k ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) ) )
94 93 notbid 
 |-  ( c = C -> ( -. ( k ( .s ` W ) c ) e. ( N ` ( U \ { c } ) ) <-> -. ( k ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) ) )
95 oveq1 
 |-  ( k = K -> ( k ( .s ` W ) C ) = ( K ( .s ` W ) C ) )
96 95 eleq1d 
 |-  ( k = K -> ( ( k ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) <-> ( K ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) ) )
97 96 notbid 
 |-  ( k = K -> ( -. ( k ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) <-> -. ( K ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) ) )
98 94 97 rspc2va 
 |-  ( ( ( C e. U /\ K e. ( F \ { O } ) ) /\ A. c e. U A. k e. ( F \ { O } ) -. ( k ( .s ` W ) c ) e. ( N ` ( U \ { c } ) ) ) -> -. ( K ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) )
99 82 83 88 98 syl21anc 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> -. ( K ( .s ` W ) C ) e. ( N ` ( U \ { C } ) ) )
100 81 99 pm2.21fal 
 |-  ( ( ( ( ph /\ x e. ( N ` ( U \ { C } ) ) ) /\ y e. ( N ` V ) ) /\ ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) -> F. )
101 23 ssdifssd 
 |-  ( ph -> ( U \ { C } ) C_ ( Base ` W ) )
102 21 58 1 lspcl 
 |-  ( ( W e. LMod /\ ( U \ { C } ) C_ ( Base ` W ) ) -> ( N ` ( U \ { C } ) ) e. ( LSubSp ` W ) )
103 14 101 102 syl2anc 
 |-  ( ph -> ( N ` ( U \ { C } ) ) e. ( LSubSp ` W ) )
104 58 lsssubg 
 |-  ( ( W e. LMod /\ ( N ` ( U \ { C } ) ) e. ( LSubSp ` W ) ) -> ( N ` ( U \ { C } ) ) e. ( SubGrp ` W ) )
105 14 103 104 syl2anc 
 |-  ( ph -> ( N ` ( U \ { C } ) ) e. ( SubGrp ` W ) )
106 21 58 1 lspcl 
 |-  ( ( W e. LMod /\ V C_ ( Base ` W ) ) -> ( N ` V ) e. ( LSubSp ` W ) )
107 14 35 106 syl2anc 
 |-  ( ph -> ( N ` V ) e. ( LSubSp ` W ) )
108 58 lsssubg 
 |-  ( ( W e. LMod /\ ( N ` V ) e. ( LSubSp ` W ) ) -> ( N ` V ) e. ( SubGrp ` W ) )
109 14 107 108 syl2anc 
 |-  ( ph -> ( N ` V ) e. ( SubGrp ` W ) )
110 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
111 21 1 110 lsmsp2 
 |-  ( ( W e. LMod /\ ( U \ { C } ) C_ ( Base ` W ) /\ V C_ ( Base ` W ) ) -> ( ( N ` ( U \ { C } ) ) ( LSSum ` W ) ( N ` V ) ) = ( N ` ( ( U \ { C } ) u. V ) ) )
112 14 101 35 111 syl3anc 
 |-  ( ph -> ( ( N ` ( U \ { C } ) ) ( LSSum ` W ) ( N ` V ) ) = ( N ` ( ( U \ { C } ) u. V ) ) )
113 65 adantr 
 |-  ( ( ph /\ C e. V ) -> C e. ( N ` U ) )
114 21 1 lspssid 
 |-  ( ( W e. LMod /\ V C_ ( Base ` W ) ) -> V C_ ( N ` V ) )
115 14 35 114 syl2anc 
 |-  ( ph -> V C_ ( N ` V ) )
116 115 sselda 
 |-  ( ( ph /\ C e. V ) -> C e. ( N ` V ) )
117 113 116 elind 
 |-  ( ( ph /\ C e. V ) -> C e. ( ( N ` U ) i^i ( N ` V ) ) )
118 6 adantr 
 |-  ( ( ph /\ C e. V ) -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
119 117 118 eleqtrd 
 |-  ( ( ph /\ C e. V ) -> C e. { .0. } )
120 elsni 
 |-  ( C e. { .0. } -> C = .0. )
121 119 120 syl 
 |-  ( ( ph /\ C e. V ) -> C = .0. )
122 2 0nellinds 
 |-  ( ( W e. LVec /\ U e. ( LIndS ` W ) ) -> -. .0. e. U )
123 3 4 122 syl2anc 
 |-  ( ph -> -. .0. e. U )
124 nelne2 
 |-  ( ( C e. U /\ -. .0. e. U ) -> C =/= .0. )
125 9 123 124 syl2anc 
 |-  ( ph -> C =/= .0. )
126 125 adantr 
 |-  ( ( ph /\ C e. V ) -> C =/= .0. )
127 126 neneqd 
 |-  ( ( ph /\ C e. V ) -> -. C = .0. )
128 121 127 pm2.65da 
 |-  ( ph -> -. C e. V )
129 disjsn 
 |-  ( ( V i^i { C } ) = (/) <-> -. C e. V )
130 128 129 sylibr 
 |-  ( ph -> ( V i^i { C } ) = (/) )
131 undif4 
 |-  ( ( V i^i { C } ) = (/) -> ( V u. ( U \ { C } ) ) = ( ( V u. U ) \ { C } ) )
132 130 131 syl 
 |-  ( ph -> ( V u. ( U \ { C } ) ) = ( ( V u. U ) \ { C } ) )
133 uncom 
 |-  ( ( U \ { C } ) u. V ) = ( V u. ( U \ { C } ) )
134 uncom 
 |-  ( U u. V ) = ( V u. U )
135 134 difeq1i 
 |-  ( ( U u. V ) \ { C } ) = ( ( V u. U ) \ { C } )
136 132 133 135 3eqtr4g 
 |-  ( ph -> ( ( U \ { C } ) u. V ) = ( ( U u. V ) \ { C } ) )
137 136 fveq2d 
 |-  ( ph -> ( N ` ( ( U \ { C } ) u. V ) ) = ( N ` ( ( U u. V ) \ { C } ) ) )
138 112 137 eqtrd 
 |-  ( ph -> ( ( N ` ( U \ { C } ) ) ( LSSum ` W ) ( N ` V ) ) = ( N ` ( ( U u. V ) \ { C } ) ) )
139 11 138 eleqtrrd 
 |-  ( ph -> ( K ( .s ` W ) C ) e. ( ( N ` ( U \ { C } ) ) ( LSSum ` W ) ( N ` V ) ) )
140 41 110 lsmelval 
 |-  ( ( ( N ` ( U \ { C } ) ) e. ( SubGrp ` W ) /\ ( N ` V ) e. ( SubGrp ` W ) ) -> ( ( K ( .s ` W ) C ) e. ( ( N ` ( U \ { C } ) ) ( LSSum ` W ) ( N ` V ) ) <-> E. x e. ( N ` ( U \ { C } ) ) E. y e. ( N ` V ) ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) ) )
141 140 biimpa 
 |-  ( ( ( ( N ` ( U \ { C } ) ) e. ( SubGrp ` W ) /\ ( N ` V ) e. ( SubGrp ` W ) ) /\ ( K ( .s ` W ) C ) e. ( ( N ` ( U \ { C } ) ) ( LSSum ` W ) ( N ` V ) ) ) -> E. x e. ( N ` ( U \ { C } ) ) E. y e. ( N ` V ) ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) )
142 105 109 139 141 syl21anc 
 |-  ( ph -> E. x e. ( N ` ( U \ { C } ) ) E. y e. ( N ` V ) ( K ( .s ` W ) C ) = ( x ( +g ` W ) y ) )
143 100 142 r19.29vva 
 |-  ( ph -> F. )