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

Metamath Proof Explorer

Theorem lspsolvlem

Description: Lemma for lspsolv . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lspsolv.v 
|- V = ( Base ` W )
lspsolv.s 
|- S = ( LSubSp ` W )
lspsolv.n 
|- N = ( LSpan ` W )
lspsolv.f 
|- F = ( Scalar ` W )
lspsolv.b 
|- B = ( Base ` F )
lspsolv.p 
|- .+ = ( +g ` W )
lspsolv.t 
|- .x. = ( .s ` W )
lspsolv.q 
|- Q = { z e. V | E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) }
lspsolv.w 
|- ( ph -> W e. LMod )
lspsolv.ss 
|- ( ph -> A C_ V )
lspsolv.y 
|- ( ph -> Y e. V )
lspsolv.x 
|- ( ph -> X e. ( N ` ( A u. { Y } ) ) )
Assertion lspsolvlem 
|- ( ph -> E. r e. B ( X .+ ( r .x. Y ) ) e. ( N ` A ) )

Proof

Step Hyp Ref Expression
1 lspsolv.v 
 |-  V = ( Base ` W )
2 lspsolv.s 
 |-  S = ( LSubSp ` W )
3 lspsolv.n 
 |-  N = ( LSpan ` W )
4 lspsolv.f 
 |-  F = ( Scalar ` W )
5 lspsolv.b 
 |-  B = ( Base ` F )
6 lspsolv.p 
 |-  .+ = ( +g ` W )
7 lspsolv.t 
 |-  .x. = ( .s ` W )
8 lspsolv.q 
 |-  Q = { z e. V | E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) }
9 lspsolv.w 
 |-  ( ph -> W e. LMod )
10 lspsolv.ss 
 |-  ( ph -> A C_ V )
11 lspsolv.y 
 |-  ( ph -> Y e. V )
12 lspsolv.x 
 |-  ( ph -> X e. ( N ` ( A u. { Y } ) ) )
13 8 ssrab3 
 |-  Q C_ V
14 13 a1i 
 |-  ( ph -> Q C_ V )
15 9 adantr 
 |-  ( ( ph /\ z e. A ) -> W e. LMod )
16 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
17 4 5 16 lmod0cl 
 |-  ( W e. LMod -> ( 0g ` F ) e. B )
18 15 17 syl 
 |-  ( ( ph /\ z e. A ) -> ( 0g ` F ) e. B )
19 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
20 1 4 7 16 19 lmod0vs 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 0g ` F ) .x. Y ) = ( 0g ` W ) )
21 9 11 20 syl2anc 
 |-  ( ph -> ( ( 0g ` F ) .x. Y ) = ( 0g ` W ) )
22 21 adantr 
 |-  ( ( ph /\ z e. A ) -> ( ( 0g ` F ) .x. Y ) = ( 0g ` W ) )
23 22 oveq2d 
 |-  ( ( ph /\ z e. A ) -> ( z .+ ( ( 0g ` F ) .x. Y ) ) = ( z .+ ( 0g ` W ) ) )
24 10 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. V )
25 1 6 19 lmod0vrid 
 |-  ( ( W e. LMod /\ z e. V ) -> ( z .+ ( 0g ` W ) ) = z )
26 15 24 25 syl2anc 
 |-  ( ( ph /\ z e. A ) -> ( z .+ ( 0g ` W ) ) = z )
27 23 26 eqtrd 
 |-  ( ( ph /\ z e. A ) -> ( z .+ ( ( 0g ` F ) .x. Y ) ) = z )
28 1 3 lspssid 
 |-  ( ( W e. LMod /\ A C_ V ) -> A C_ ( N ` A ) )
29 9 10 28 syl2anc 
 |-  ( ph -> A C_ ( N ` A ) )
30 29 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. ( N ` A ) )
31 27 30 eqeltrd 
 |-  ( ( ph /\ z e. A ) -> ( z .+ ( ( 0g ` F ) .x. Y ) ) e. ( N ` A ) )
32 oveq1 
 |-  ( r = ( 0g ` F ) -> ( r .x. Y ) = ( ( 0g ` F ) .x. Y ) )
33 32 oveq2d 
 |-  ( r = ( 0g ` F ) -> ( z .+ ( r .x. Y ) ) = ( z .+ ( ( 0g ` F ) .x. Y ) ) )
34 33 eleq1d 
 |-  ( r = ( 0g ` F ) -> ( ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( z .+ ( ( 0g ` F ) .x. Y ) ) e. ( N ` A ) ) )
35 34 rspcev 
 |-  ( ( ( 0g ` F ) e. B /\ ( z .+ ( ( 0g ` F ) .x. Y ) ) e. ( N ` A ) ) -> E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) )
36 18 31 35 syl2anc 
 |-  ( ( ph /\ z e. A ) -> E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) )
37 10 36 ssrabdv 
 |-  ( ph -> A C_ { z e. V | E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) } )
38 37 8 sseqtrrdi 
 |-  ( ph -> A C_ Q )
39 4 lmodfgrp 
 |-  ( W e. LMod -> F e. Grp )
40 9 39 syl 
 |-  ( ph -> F e. Grp )
41 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
42 4 5 41 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` F ) e. B )
43 9 42 syl 
 |-  ( ph -> ( 1r ` F ) e. B )
44 eqid 
 |-  ( invg ` F ) = ( invg ` F )
45 5 44 grpinvcl 
 |-  ( ( F e. Grp /\ ( 1r ` F ) e. B ) -> ( ( invg ` F ) ` ( 1r ` F ) ) e. B )
46 40 43 45 syl2anc 
 |-  ( ph -> ( ( invg ` F ) ` ( 1r ` F ) ) e. B )
47 eqid 
 |-  ( invg ` W ) = ( invg ` W )
48 1 47 4 7 41 44 lmodvneg1 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) = ( ( invg ` W ) ` Y ) )
49 9 11 48 syl2anc 
 |-  ( ph -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) = ( ( invg ` W ) ` Y ) )
50 49 oveq2d 
 |-  ( ph -> ( Y .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) ) = ( Y .+ ( ( invg ` W ) ` Y ) ) )
51 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
52 9 51 syl 
 |-  ( ph -> W e. Grp )
53 1 6 19 47 grprinv 
 |-  ( ( W e. Grp /\ Y e. V ) -> ( Y .+ ( ( invg ` W ) ` Y ) ) = ( 0g ` W ) )
54 52 11 53 syl2anc 
 |-  ( ph -> ( Y .+ ( ( invg ` W ) ` Y ) ) = ( 0g ` W ) )
55 50 54 eqtrd 
 |-  ( ph -> ( Y .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) ) = ( 0g ` W ) )
56 1 2 3 lspcl 
 |-  ( ( W e. LMod /\ A C_ V ) -> ( N ` A ) e. S )
57 9 10 56 syl2anc 
 |-  ( ph -> ( N ` A ) e. S )
58 19 2 lss0cl 
 |-  ( ( W e. LMod /\ ( N ` A ) e. S ) -> ( 0g ` W ) e. ( N ` A ) )
59 9 57 58 syl2anc 
 |-  ( ph -> ( 0g ` W ) e. ( N ` A ) )
60 55 59 eqeltrd 
 |-  ( ph -> ( Y .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) ) e. ( N ` A ) )
61 oveq1 
 |-  ( r = ( ( invg ` F ) ` ( 1r ` F ) ) -> ( r .x. Y ) = ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) )
62 61 oveq2d 
 |-  ( r = ( ( invg ` F ) ` ( 1r ` F ) ) -> ( Y .+ ( r .x. Y ) ) = ( Y .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) ) )
63 62 eleq1d 
 |-  ( r = ( ( invg ` F ) ` ( 1r ` F ) ) -> ( ( Y .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( Y .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) ) e. ( N ` A ) ) )
64 63 rspcev 
 |-  ( ( ( ( invg ` F ) ` ( 1r ` F ) ) e. B /\ ( Y .+ ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. Y ) ) e. ( N ` A ) ) -> E. r e. B ( Y .+ ( r .x. Y ) ) e. ( N ` A ) )
65 46 60 64 syl2anc 
 |-  ( ph -> E. r e. B ( Y .+ ( r .x. Y ) ) e. ( N ` A ) )
66 oveq1 
 |-  ( z = Y -> ( z .+ ( r .x. Y ) ) = ( Y .+ ( r .x. Y ) ) )
67 66 eleq1d 
 |-  ( z = Y -> ( ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( Y .+ ( r .x. Y ) ) e. ( N ` A ) ) )
68 67 rexbidv 
 |-  ( z = Y -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. r e. B ( Y .+ ( r .x. Y ) ) e. ( N ` A ) ) )
69 68 8 elrab2 
 |-  ( Y e. Q <-> ( Y e. V /\ E. r e. B ( Y .+ ( r .x. Y ) ) e. ( N ` A ) ) )
70 11 65 69 sylanbrc 
 |-  ( ph -> Y e. Q )
71 70 snssd 
 |-  ( ph -> { Y } C_ Q )
72 38 71 unssd 
 |-  ( ph -> ( A u. { Y } ) C_ Q )
73 1 3 lspss 
 |-  ( ( W e. LMod /\ Q C_ V /\ ( A u. { Y } ) C_ Q ) -> ( N ` ( A u. { Y } ) ) C_ ( N ` Q ) )
74 9 14 72 73 syl3anc 
 |-  ( ph -> ( N ` ( A u. { Y } ) ) C_ ( N ` Q ) )
75 4 a1i 
 |-  ( ph -> F = ( Scalar ` W ) )
76 5 a1i 
 |-  ( ph -> B = ( Base ` F ) )
77 1 a1i 
 |-  ( ph -> V = ( Base ` W ) )
78 6 a1i 
 |-  ( ph -> .+ = ( +g ` W ) )
79 7 a1i 
 |-  ( ph -> .x. = ( .s ` W ) )
80 2 a1i 
 |-  ( ph -> S = ( LSubSp ` W ) )
81 70 ne0d 
 |-  ( ph -> Q =/= (/) )
82 oveq1 
 |-  ( z = x -> ( z .+ ( r .x. Y ) ) = ( x .+ ( r .x. Y ) ) )
83 82 eleq1d 
 |-  ( z = x -> ( ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( x .+ ( r .x. Y ) ) e. ( N ` A ) ) )
84 83 rexbidv 
 |-  ( z = x -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. r e. B ( x .+ ( r .x. Y ) ) e. ( N ` A ) ) )
85 oveq1 
 |-  ( r = s -> ( r .x. Y ) = ( s .x. Y ) )
86 85 oveq2d 
 |-  ( r = s -> ( x .+ ( r .x. Y ) ) = ( x .+ ( s .x. Y ) ) )
87 86 eleq1d 
 |-  ( r = s -> ( ( x .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( x .+ ( s .x. Y ) ) e. ( N ` A ) ) )
88 87 cbvrexvw 
 |-  ( E. r e. B ( x .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) )
89 84 88 bitrdi 
 |-  ( z = x -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) ) )
90 89 8 elrab2 
 |-  ( x e. Q <-> ( x e. V /\ E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) ) )
91 oveq1 
 |-  ( z = y -> ( z .+ ( r .x. Y ) ) = ( y .+ ( r .x. Y ) ) )
92 91 eleq1d 
 |-  ( z = y -> ( ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( y .+ ( r .x. Y ) ) e. ( N ` A ) ) )
93 92 rexbidv 
 |-  ( z = y -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. r e. B ( y .+ ( r .x. Y ) ) e. ( N ` A ) ) )
94 oveq1 
 |-  ( r = t -> ( r .x. Y ) = ( t .x. Y ) )
95 94 oveq2d 
 |-  ( r = t -> ( y .+ ( r .x. Y ) ) = ( y .+ ( t .x. Y ) ) )
96 95 eleq1d 
 |-  ( r = t -> ( ( y .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) )
97 96 cbvrexvw 
 |-  ( E. r e. B ( y .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) )
98 93 97 bitrdi 
 |-  ( z = y -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) )
99 98 8 elrab2 
 |-  ( y e. Q <-> ( y e. V /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) )
100 90 99 anbi12i 
 |-  ( ( x e. Q /\ y e. Q ) <-> ( ( x e. V /\ E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) ) /\ ( y e. V /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) )
101 an4 
 |-  ( ( ( x e. V /\ E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) ) /\ ( y e. V /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) <-> ( ( x e. V /\ y e. V ) /\ ( E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) )
102 100 101 bitri 
 |-  ( ( x e. Q /\ y e. Q ) <-> ( ( x e. V /\ y e. V ) /\ ( E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) )
103 reeanv 
 |-  ( E. s e. B E. t e. B ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) <-> ( E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) )
104 simp1ll 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ph )
105 104 9 syl 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> W e. LMod )
106 simp1lr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> a e. B )
107 simp1rl 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> x e. V )
108 1 4 7 5 lmodvscl 
 |-  ( ( W e. LMod /\ a e. B /\ x e. V ) -> ( a .x. x ) e. V )
109 105 106 107 108 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( a .x. x ) e. V )
110 simp1rr 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> y e. V )
111 1 6 lmodvacl 
 |-  ( ( W e. LMod /\ ( a .x. x ) e. V /\ y e. V ) -> ( ( a .x. x ) .+ y ) e. V )
112 105 109 110 111 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a .x. x ) .+ y ) e. V )
113 simp2l 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> s e. B )
114 eqid 
 |-  ( .r ` F ) = ( .r ` F )
115 4 5 114 lmodmcl 
 |-  ( ( W e. LMod /\ a e. B /\ s e. B ) -> ( a ( .r ` F ) s ) e. B )
116 105 106 113 115 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( a ( .r ` F ) s ) e. B )
117 simp2r 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> t e. B )
118 eqid 
 |-  ( +g ` F ) = ( +g ` F )
119 4 5 118 lmodacl 
 |-  ( ( W e. LMod /\ ( a ( .r ` F ) s ) e. B /\ t e. B ) -> ( ( a ( .r ` F ) s ) ( +g ` F ) t ) e. B )
120 105 116 117 119 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a ( .r ` F ) s ) ( +g ` F ) t ) e. B )
121 104 11 syl 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> Y e. V )
122 1 4 7 5 lmodvscl 
 |-  ( ( W e. LMod /\ s e. B /\ Y e. V ) -> ( s .x. Y ) e. V )
123 105 113 121 122 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( s .x. Y ) e. V )
124 1 4 7 5 lmodvscl 
 |-  ( ( W e. LMod /\ a e. B /\ ( s .x. Y ) e. V ) -> ( a .x. ( s .x. Y ) ) e. V )
125 105 106 123 124 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( a .x. ( s .x. Y ) ) e. V )
126 1 4 7 5 lmodvscl 
 |-  ( ( W e. LMod /\ t e. B /\ Y e. V ) -> ( t .x. Y ) e. V )
127 105 117 121 126 syl3anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( t .x. Y ) e. V )
128 1 6 lmod4 
 |-  ( ( W e. LMod /\ ( ( a .x. x ) e. V /\ y e. V ) /\ ( ( a .x. ( s .x. Y ) ) e. V /\ ( t .x. Y ) e. V ) ) -> ( ( ( a .x. x ) .+ y ) .+ ( ( a .x. ( s .x. Y ) ) .+ ( t .x. Y ) ) ) = ( ( ( a .x. x ) .+ ( a .x. ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) )
129 105 109 110 125 127 128 syl122anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a .x. x ) .+ y ) .+ ( ( a .x. ( s .x. Y ) ) .+ ( t .x. Y ) ) ) = ( ( ( a .x. x ) .+ ( a .x. ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) )
130 1 6 4 7 5 118 lmodvsdir 
 |-  ( ( W e. LMod /\ ( ( a ( .r ` F ) s ) e. B /\ t e. B /\ Y e. V ) ) -> ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) = ( ( ( a ( .r ` F ) s ) .x. Y ) .+ ( t .x. Y ) ) )
131 105 116 117 121 130 syl13anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) = ( ( ( a ( .r ` F ) s ) .x. Y ) .+ ( t .x. Y ) ) )
132 1 4 7 5 114 lmodvsass 
 |-  ( ( W e. LMod /\ ( a e. B /\ s e. B /\ Y e. V ) ) -> ( ( a ( .r ` F ) s ) .x. Y ) = ( a .x. ( s .x. Y ) ) )
133 105 106 113 121 132 syl13anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a ( .r ` F ) s ) .x. Y ) = ( a .x. ( s .x. Y ) ) )
134 133 oveq1d 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a ( .r ` F ) s ) .x. Y ) .+ ( t .x. Y ) ) = ( ( a .x. ( s .x. Y ) ) .+ ( t .x. Y ) ) )
135 131 134 eqtrd 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) = ( ( a .x. ( s .x. Y ) ) .+ ( t .x. Y ) ) )
136 135 oveq2d 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a .x. x ) .+ y ) .+ ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) ) = ( ( ( a .x. x ) .+ y ) .+ ( ( a .x. ( s .x. Y ) ) .+ ( t .x. Y ) ) ) )
137 1 6 4 7 5 lmodvsdi 
 |-  ( ( W e. LMod /\ ( a e. B /\ x e. V /\ ( s .x. Y ) e. V ) ) -> ( a .x. ( x .+ ( s .x. Y ) ) ) = ( ( a .x. x ) .+ ( a .x. ( s .x. Y ) ) ) )
138 105 106 107 123 137 syl13anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( a .x. ( x .+ ( s .x. Y ) ) ) = ( ( a .x. x ) .+ ( a .x. ( s .x. Y ) ) ) )
139 138 oveq1d 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a .x. ( x .+ ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) = ( ( ( a .x. x ) .+ ( a .x. ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) )
140 129 136 139 3eqtr4d 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a .x. x ) .+ y ) .+ ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) ) = ( ( a .x. ( x .+ ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) )
141 104 57 syl 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( N ` A ) e. S )
142 simp3l 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( x .+ ( s .x. Y ) ) e. ( N ` A ) )
143 simp3r 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( y .+ ( t .x. Y ) ) e. ( N ` A ) )
144 4 5 6 7 2 lsscl 
 |-  ( ( ( N ` A ) e. S /\ ( a e. B /\ ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a .x. ( x .+ ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) e. ( N ` A ) )
145 141 106 142 143 144 syl13anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a .x. ( x .+ ( s .x. Y ) ) ) .+ ( y .+ ( t .x. Y ) ) ) e. ( N ` A ) )
146 140 145 eqeltrd 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( ( a .x. x ) .+ y ) .+ ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) ) e. ( N ` A ) )
147 oveq1 
 |-  ( r = ( ( a ( .r ` F ) s ) ( +g ` F ) t ) -> ( r .x. Y ) = ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) )
148 147 oveq2d 
 |-  ( r = ( ( a ( .r ` F ) s ) ( +g ` F ) t ) -> ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) = ( ( ( a .x. x ) .+ y ) .+ ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) ) )
149 148 eleq1d 
 |-  ( r = ( ( a ( .r ` F ) s ) ( +g ` F ) t ) -> ( ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( ( ( a .x. x ) .+ y ) .+ ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) ) e. ( N ` A ) ) )
150 149 rspcev 
 |-  ( ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) e. B /\ ( ( ( a .x. x ) .+ y ) .+ ( ( ( a ( .r ` F ) s ) ( +g ` F ) t ) .x. Y ) ) e. ( N ` A ) ) -> E. r e. B ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) e. ( N ` A ) )
151 120 146 150 syl2anc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> E. r e. B ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) e. ( N ` A ) )
152 oveq1 
 |-  ( z = ( ( a .x. x ) .+ y ) -> ( z .+ ( r .x. Y ) ) = ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) )
153 152 eleq1d 
 |-  ( z = ( ( a .x. x ) .+ y ) -> ( ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) e. ( N ` A ) ) )
154 153 rexbidv 
 |-  ( z = ( ( a .x. x ) .+ y ) -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. r e. B ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) e. ( N ` A ) ) )
155 154 8 elrab2 
 |-  ( ( ( a .x. x ) .+ y ) e. Q <-> ( ( ( a .x. x ) .+ y ) e. V /\ E. r e. B ( ( ( a .x. x ) .+ y ) .+ ( r .x. Y ) ) e. ( N ` A ) ) )
156 112 151 155 sylanbrc 
 |-  ( ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) /\ ( s e. B /\ t e. B ) /\ ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a .x. x ) .+ y ) e. Q )
157 156 3exp 
 |-  ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) -> ( ( s e. B /\ t e. B ) -> ( ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) -> ( ( a .x. x ) .+ y ) e. Q ) ) )
158 157 rexlimdvv 
 |-  ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) -> ( E. s e. B E. t e. B ( ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) -> ( ( a .x. x ) .+ y ) e. Q ) )
159 103 158 biimtrrid 
 |-  ( ( ( ph /\ a e. B ) /\ ( x e. V /\ y e. V ) ) -> ( ( E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) -> ( ( a .x. x ) .+ y ) e. Q ) )
160 159 expimpd 
 |-  ( ( ph /\ a e. B ) -> ( ( ( x e. V /\ y e. V ) /\ ( E. s e. B ( x .+ ( s .x. Y ) ) e. ( N ` A ) /\ E. t e. B ( y .+ ( t .x. Y ) ) e. ( N ` A ) ) ) -> ( ( a .x. x ) .+ y ) e. Q ) )
161 102 160 biimtrid 
 |-  ( ( ph /\ a e. B ) -> ( ( x e. Q /\ y e. Q ) -> ( ( a .x. x ) .+ y ) e. Q ) )
162 161 exp4b 
 |-  ( ph -> ( a e. B -> ( x e. Q -> ( y e. Q -> ( ( a .x. x ) .+ y ) e. Q ) ) ) )
163 162 3imp2 
 |-  ( ( ph /\ ( a e. B /\ x e. Q /\ y e. Q ) ) -> ( ( a .x. x ) .+ y ) e. Q )
164 75 76 77 78 79 80 14 81 163 islssd 
 |-  ( ph -> Q e. S )
165 2 3 lspid 
 |-  ( ( W e. LMod /\ Q e. S ) -> ( N ` Q ) = Q )
166 9 164 165 syl2anc 
 |-  ( ph -> ( N ` Q ) = Q )
167 74 166 sseqtrd 
 |-  ( ph -> ( N ` ( A u. { Y } ) ) C_ Q )
168 167 12 sseldd 
 |-  ( ph -> X e. Q )
169 oveq1 
 |-  ( z = X -> ( z .+ ( r .x. Y ) ) = ( X .+ ( r .x. Y ) ) )
170 169 eleq1d 
 |-  ( z = X -> ( ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> ( X .+ ( r .x. Y ) ) e. ( N ` A ) ) )
171 170 rexbidv 
 |-  ( z = X -> ( E. r e. B ( z .+ ( r .x. Y ) ) e. ( N ` A ) <-> E. r e. B ( X .+ ( r .x. Y ) ) e. ( N ` A ) ) )
172 171 8 elrab2 
 |-  ( X e. Q <-> ( X e. V /\ E. r e. B ( X .+ ( r .x. Y ) ) e. ( N ` A ) ) )
173 172 simprbi 
 |-  ( X e. Q -> E. r e. B ( X .+ ( r .x. Y ) ) e. ( N ` A ) )
174 168 173 syl 
 |-  ( ph -> E. r e. B ( X .+ ( r .x. Y ) ) e. ( N ` A ) )