Metamath Proof Explorer

Theorem lbsextlem4

Description: Lemma for lbsext . lbsextlem3 satisfies the conditions for the application of Zorn's lemma zorn (thus invoking AC), and so there is a maximal linearly independent set extending C . Here we prove that such a set is a basis. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v 
|- V = ( Base ` W )
lbsext.j 
|- J = ( LBasis ` W )
lbsext.n 
|- N = ( LSpan ` W )
lbsext.w 
|- ( ph -> W e. LVec )
lbsext.c 
|- ( ph -> C C_ V )
lbsext.x 
|- ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
lbsext.s 
|- S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
lbsext.k 
|- ( ph -> ~P V e. dom card )
Assertion lbsextlem4 
|- ( ph -> E. s e. J C C_ s )

Proof

Step Hyp Ref Expression
1 lbsext.v 
 |-  V = ( Base ` W )
2 lbsext.j 
 |-  J = ( LBasis ` W )
3 lbsext.n 
 |-  N = ( LSpan ` W )
4 lbsext.w 
 |-  ( ph -> W e. LVec )
5 lbsext.c 
 |-  ( ph -> C C_ V )
6 lbsext.x 
 |-  ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
7 lbsext.s 
 |-  S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
8 lbsext.k 
 |-  ( ph -> ~P V e. dom card )
9 7 ssrab3 
 |-  S C_ ~P V
10 ssnum 
 |-  ( ( ~P V e. dom card /\ S C_ ~P V ) -> S e. dom card )
11 8 9 10 sylancl 
 |-  ( ph -> S e. dom card )
12 1 2 3 4 5 6 7 lbsextlem1 
 |-  ( ph -> S =/= (/) )
13 4 adantr 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> W e. LVec )
14 5 adantr 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> C C_ V )
15 6 adantr 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
16 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
17 simpr1 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> y C_ S )
18 simpr2 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> y =/= (/) )
19 simpr3 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> [C.] Or y )
20 eqid 
 |-  U_ u e. y ( N ` ( u \ { x } ) ) = U_ u e. y ( N ` ( u \ { x } ) )
21 1 2 3 13 14 15 7 16 17 18 19 20 lbsextlem3 
 |-  ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [C.] Or y ) ) -> U. y e. S )
22 21 ex 
 |-  ( ph -> ( ( y C_ S /\ y =/= (/) /\ [C.] Or y ) -> U. y e. S ) )
23 22 alrimiv 
 |-  ( ph -> A. y ( ( y C_ S /\ y =/= (/) /\ [C.] Or y ) -> U. y e. S ) )
24 zornn0g 
 |-  ( ( S e. dom card /\ S =/= (/) /\ A. y ( ( y C_ S /\ y =/= (/) /\ [C.] Or y ) -> U. y e. S ) ) -> E. s e. S A. t e. S -. s C. t )
25 11 12 23 24 syl3anc 
 |-  ( ph -> E. s e. S A. t e. S -. s C. t )
26 simprl 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. S )
27 sseq2 
 |-  ( z = s -> ( C C_ z <-> C C_ s ) )
28 difeq1 
 |-  ( z = s -> ( z \ { x } ) = ( s \ { x } ) )
29 28 fveq2d 
 |-  ( z = s -> ( N ` ( z \ { x } ) ) = ( N ` ( s \ { x } ) ) )
30 29 eleq2d 
 |-  ( z = s -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( s \ { x } ) ) ) )
31 30 notbid 
 |-  ( z = s -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( s \ { x } ) ) ) )
32 31 raleqbi1dv 
 |-  ( z = s -> ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) )
33 27 32 anbi12d 
 |-  ( z = s -> ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) <-> ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
34 33 7 elrab2 
 |-  ( s e. S <-> ( s e. ~P V /\ ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
35 26 34 sylib 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s e. ~P V /\ ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
36 35 simpld 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. ~P V )
37 36 elpwid 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ V )
38 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
39 4 38 syl 
 |-  ( ph -> W e. LMod )
40 39 adantr 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LMod )
41 1 3 lspssv 
 |-  ( ( W e. LMod /\ s C_ V ) -> ( N ` s ) C_ V )
42 40 37 41 syl2anc 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) C_ V )
43 ssun1 
 |-  s C_ ( s u. { w } )
44 43 a1i 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ ( s u. { w } ) )
45 ssun2 
 |-  { w } C_ ( s u. { w } )
46 vsnid 
 |-  w e. { w }
47 45 46 sselii 
 |-  w e. ( s u. { w } )
48 1 3 lspssid 
 |-  ( ( W e. LMod /\ s C_ V ) -> s C_ ( N ` s ) )
49 40 37 48 syl2anc 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ ( N ` s ) )
50 49 adantr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ ( N ` s ) )
51 eldifn 
 |-  ( w e. ( V \ ( N ` s ) ) -> -. w e. ( N ` s ) )
52 51 adantl 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` s ) )
53 50 52 ssneldd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. s )
54 nelne1 
 |-  ( ( w e. ( s u. { w } ) /\ -. w e. s ) -> ( s u. { w } ) =/= s )
55 47 53 54 sylancr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) =/= s )
56 55 necomd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s =/= ( s u. { w } ) )
57 df-pss 
 |-  ( s C. ( s u. { w } ) <-> ( s C_ ( s u. { w } ) /\ s =/= ( s u. { w } ) ) )
58 44 56 57 sylanbrc 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C. ( s u. { w } ) )
59 psseq2 
 |-  ( t = ( s u. { w } ) -> ( s C. t <-> s C. ( s u. { w } ) ) )
60 59 notbid 
 |-  ( t = ( s u. { w } ) -> ( -. s C. t <-> -. s C. ( s u. { w } ) ) )
61 simplrr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> A. t e. S -. s C. t )
62 37 adantr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ V )
63 eldifi 
 |-  ( w e. ( V \ ( N ` s ) ) -> w e. V )
64 63 adantl 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> w e. V )
65 64 snssd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> { w } C_ V )
66 62 65 unssd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) C_ V )
67 1 fvexi 
 |-  V e. _V
68 67 elpw2 
 |-  ( ( s u. { w } ) e. ~P V <-> ( s u. { w } ) C_ V )
69 66 68 sylibr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. ~P V )
70 35 simprd 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) )
71 70 simpld 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> C C_ s )
72 71 adantr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ s )
73 72 43 sstrdi 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ ( s u. { w } ) )
74 4 ad2antrr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> W e. LVec )
75 37 adantr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> s C_ V )
76 75 ssdifssd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( s \ { x } ) C_ V )
77 64 adantrr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> w e. V )
78 simprrr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> x e. ( N ` ( ( s u. { w } ) \ { x } ) ) )
79 difundir 
 |-  ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) )
80 simprrl 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> x e. s )
81 53 adantrr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> -. w e. s )
82 nelne2 
 |-  ( ( x e. s /\ -. w e. s ) -> x =/= w )
83 80 81 82 syl2anc 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> x =/= w )
84 nelsn 
 |-  ( x =/= w -> -. x e. { w } )
85 83 84 syl 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> -. x e. { w } )
86 disjsn 
 |-  ( ( { w } i^i { x } ) = (/) <-> -. x e. { w } )
87 85 86 sylibr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( { w } i^i { x } ) = (/) )
88 disj3 
 |-  ( ( { w } i^i { x } ) = (/) <-> { w } = ( { w } \ { x } ) )
89 87 88 sylib 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> { w } = ( { w } \ { x } ) )
90 89 uneq2d 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( ( s \ { x } ) u. { w } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) ) )
91 79 90 eqtr4id 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. { w } ) )
92 91 fveq2d 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( ( s \ { x } ) u. { w } ) ) )
93 78 92 eleqtrd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> x e. ( N ` ( ( s \ { x } ) u. { w } ) ) )
94 70 simprd 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> A. x e. s -. x e. ( N ` ( s \ { x } ) ) )
95 94 adantr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> A. x e. s -. x e. ( N ` ( s \ { x } ) ) )
96 rsp 
 |-  ( A. x e. s -. x e. ( N ` ( s \ { x } ) ) -> ( x e. s -> -. x e. ( N ` ( s \ { x } ) ) ) )
97 95 80 96 sylc 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> -. x e. ( N ` ( s \ { x } ) ) )
98 93 97 eldifd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> x e. ( ( N ` ( ( s \ { x } ) u. { w } ) ) \ ( N ` ( s \ { x } ) ) ) )
99 1 16 3 lspsolv 
 |-  ( ( W e. LVec /\ ( ( s \ { x } ) C_ V /\ w e. V /\ x e. ( ( N ` ( ( s \ { x } ) u. { w } ) ) \ ( N ` ( s \ { x } ) ) ) ) ) -> w e. ( N ` ( ( s \ { x } ) u. { x } ) ) )
100 74 76 77 98 99 syl13anc 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> w e. ( N ` ( ( s \ { x } ) u. { x } ) ) )
101 undif1 
 |-  ( ( s \ { x } ) u. { x } ) = ( s u. { x } )
102 80 snssd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> { x } C_ s )
103 ssequn2 
 |-  ( { x } C_ s <-> ( s u. { x } ) = s )
104 102 103 sylib 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( s u. { x } ) = s )
105 101 104 eqtrid 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( ( s \ { x } ) u. { x } ) = s )
106 105 fveq2d 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> ( N ` ( ( s \ { x } ) u. { x } ) ) = ( N ` s ) )
107 100 106 eleqtrd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ ( w e. ( V \ ( N ` s ) ) /\ ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) ) -> w e. ( N ` s ) )
108 107 expr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) -> w e. ( N ` s ) ) )
109 52 108 mtod 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
110 imnan 
 |-  ( ( x e. s -> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) <-> -. ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
111 109 110 sylibr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( x e. s -> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
112 111 ralrimiv 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> A. x e. s -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) )
113 difssd 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s \ { w } ) C_ s )
114 1 3 lspss 
 |-  ( ( W e. LMod /\ s C_ V /\ ( s \ { w } ) C_ s ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
115 40 37 113 114 syl3anc 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
116 115 adantr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
117 116 52 ssneldd 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` ( s \ { w } ) ) )
118 vex 
 |-  w e. _V
119 id 
 |-  ( x = w -> x = w )
120 sneq 
 |-  ( x = w -> { x } = { w } )
121 120 difeq2d 
 |-  ( x = w -> ( ( s u. { w } ) \ { x } ) = ( ( s u. { w } ) \ { w } ) )
122 difun2 
 |-  ( ( s u. { w } ) \ { w } ) = ( s \ { w } )
123 121 122 eqtrdi 
 |-  ( x = w -> ( ( s u. { w } ) \ { x } ) = ( s \ { w } ) )
124 123 fveq2d 
 |-  ( x = w -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( s \ { w } ) ) )
125 119 124 eleq12d 
 |-  ( x = w -> ( x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> w e. ( N ` ( s \ { w } ) ) ) )
126 125 notbid 
 |-  ( x = w -> ( -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) ) )
127 118 126 ralsn 
 |-  ( A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) )
128 117 127 sylibr 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) )
129 ralun 
 |-  ( ( A. x e. s -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) /\ A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) -> A. x e. ( s u. { w } ) -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) )
130 112 128 129 syl2anc 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> A. x e. ( s u. { w } ) -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) )
131 73 130 jca 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( C C_ ( s u. { w } ) /\ A. x e. ( s u. { w } ) -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
132 sseq2 
 |-  ( z = ( s u. { w } ) -> ( C C_ z <-> C C_ ( s u. { w } ) ) )
133 difeq1 
 |-  ( z = ( s u. { w } ) -> ( z \ { x } ) = ( ( s u. { w } ) \ { x } ) )
134 133 fveq2d 
 |-  ( z = ( s u. { w } ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( s u. { w } ) \ { x } ) ) )
135 134 eleq2d 
 |-  ( z = ( s u. { w } ) -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
136 135 notbid 
 |-  ( z = ( s u. { w } ) -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
137 136 raleqbi1dv 
 |-  ( z = ( s u. { w } ) -> ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. x e. ( s u. { w } ) -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
138 132 137 anbi12d 
 |-  ( z = ( s u. { w } ) -> ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) <-> ( C C_ ( s u. { w } ) /\ A. x e. ( s u. { w } ) -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) )
139 138 7 elrab2 
 |-  ( ( s u. { w } ) e. S <-> ( ( s u. { w } ) e. ~P V /\ ( C C_ ( s u. { w } ) /\ A. x e. ( s u. { w } ) -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) ) )
140 69 131 139 sylanbrc 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. S )
141 60 61 140 rspcdva 
 |-  ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. s C. ( s u. { w } ) )
142 58 141 pm2.65da 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> -. w e. ( V \ ( N ` s ) ) )
143 142 eq0rdv 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( V \ ( N ` s ) ) = (/) )
144 ssdif0 
 |-  ( V C_ ( N ` s ) <-> ( V \ ( N ` s ) ) = (/) )
145 143 144 sylibr 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> V C_ ( N ` s ) )
146 42 145 eqssd 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) = V )
147 4 adantr 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LVec )
148 1 2 3 islbs2 
 |-  ( W e. LVec -> ( s e. J <-> ( s C_ V /\ ( N ` s ) = V /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
149 147 148 syl 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s e. J <-> ( s C_ V /\ ( N ` s ) = V /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
150 37 146 94 149 mpbir3and 
 |-  ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. J )
151 25 150 71 reximssdv 
 |-  ( ph -> E. s e. J C C_ s )