Metamath Proof Explorer

Theorem lbsextlem3

Description: Lemma for lbsext . A chain in S has an upper bound in S . (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.p 
|- P = ( LSubSp ` W )
lbsext.a 
|- ( ph -> A C_ S )
lbsext.z 
|- ( ph -> A =/= (/) )
lbsext.r 
|- ( ph -> [C.] Or A )
lbsext.t 
|- T = U_ u e. A ( N ` ( u \ { x } ) )
Assertion lbsextlem3 
|- ( ph -> U. A e. 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.p 
 |-  P = ( LSubSp ` W )
9 lbsext.a 
 |-  ( ph -> A C_ S )
10 lbsext.z 
 |-  ( ph -> A =/= (/) )
11 lbsext.r 
 |-  ( ph -> [C.] Or A )
12 lbsext.t 
 |-  T = U_ u e. A ( N ` ( u \ { x } ) )
13 7 ssrab3 
 |-  S C_ ~P V
14 9 13 sstrdi 
 |-  ( ph -> A C_ ~P V )
15 sspwuni 
 |-  ( A C_ ~P V <-> U. A C_ V )
16 14 15 sylib 
 |-  ( ph -> U. A C_ V )
17 1 fvexi 
 |-  V e. _V
18 17 elpw2 
 |-  ( U. A e. ~P V <-> U. A C_ V )
19 16 18 sylibr 
 |-  ( ph -> U. A e. ~P V )
20 ssintub 
 |-  C C_ |^| { z e. ~P V | C C_ z }
21 simpl 
 |-  ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) -> C C_ z )
22 21 a1i 
 |-  ( z e. ~P V -> ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) -> C C_ z ) )
23 22 ss2rabi 
 |-  { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } C_ { z e. ~P V | C C_ z }
24 7 23 eqsstri 
 |-  S C_ { z e. ~P V | C C_ z }
25 9 24 sstrdi 
 |-  ( ph -> A C_ { z e. ~P V | C C_ z } )
26 intss 
 |-  ( A C_ { z e. ~P V | C C_ z } -> |^| { z e. ~P V | C C_ z } C_ |^| A )
27 25 26 syl 
 |-  ( ph -> |^| { z e. ~P V | C C_ z } C_ |^| A )
28 20 27 sstrid 
 |-  ( ph -> C C_ |^| A )
29 intssuni 
 |-  ( A =/= (/) -> |^| A C_ U. A )
30 10 29 syl 
 |-  ( ph -> |^| A C_ U. A )
31 28 30 sstrd 
 |-  ( ph -> C C_ U. A )
32 eluni2 
 |-  ( x e. U. A <-> E. y e. A x e. y )
33 simpll1 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ph )
34 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
35 4 34 syl 
 |-  ( ph -> W e. LMod )
36 33 35 syl 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> W e. LMod )
37 33 9 syl 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> A C_ S )
38 33 11 syl 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> [C.] Or A )
39 simpll2 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> y e. A )
40 simplr 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> u e. A )
41 sorpssun 
 |-  ( ( [C.] Or A /\ ( y e. A /\ u e. A ) ) -> ( y u. u ) e. A )
42 38 39 40 41 syl12anc 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( y u. u ) e. A )
43 37 42 sseldd 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( y u. u ) e. S )
44 13 43 sselid 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( y u. u ) e. ~P V )
45 44 elpwid 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( y u. u ) C_ V )
46 45 ssdifssd 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( ( y u. u ) \ { x } ) C_ V )
47 ssun2 
 |-  u C_ ( y u. u )
48 ssdif 
 |-  ( u C_ ( y u. u ) -> ( u \ { x } ) C_ ( ( y u. u ) \ { x } ) )
49 47 48 mp1i 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( u \ { x } ) C_ ( ( y u. u ) \ { x } ) )
50 1 3 lspss 
 |-  ( ( W e. LMod /\ ( ( y u. u ) \ { x } ) C_ V /\ ( u \ { x } ) C_ ( ( y u. u ) \ { x } ) ) -> ( N ` ( u \ { x } ) ) C_ ( N ` ( ( y u. u ) \ { x } ) ) )
51 36 46 49 50 syl3anc 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> ( N ` ( u \ { x } ) ) C_ ( N ` ( ( y u. u ) \ { x } ) ) )
52 simpr 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> x e. ( N ` ( u \ { x } ) ) )
53 51 52 sseldd 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> x e. ( N ` ( ( y u. u ) \ { x } ) ) )
54 sseq2 
 |-  ( z = ( y u. u ) -> ( C C_ z <-> C C_ ( y u. u ) ) )
55 difeq1 
 |-  ( z = ( y u. u ) -> ( z \ { x } ) = ( ( y u. u ) \ { x } ) )
56 55 fveq2d 
 |-  ( z = ( y u. u ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( y u. u ) \ { x } ) ) )
57 56 eleq2d 
 |-  ( z = ( y u. u ) -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( ( y u. u ) \ { x } ) ) ) )
58 57 notbid 
 |-  ( z = ( y u. u ) -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( ( y u. u ) \ { x } ) ) ) )
59 58 raleqbi1dv 
 |-  ( z = ( y u. u ) -> ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) ) )
60 54 59 anbi12d 
 |-  ( z = ( y u. u ) -> ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) <-> ( C C_ ( y u. u ) /\ A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) ) ) )
61 60 7 elrab2 
 |-  ( ( y u. u ) e. S <-> ( ( y u. u ) e. ~P V /\ ( C C_ ( y u. u ) /\ A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) ) ) )
62 61 simprbi 
 |-  ( ( y u. u ) e. S -> ( C C_ ( y u. u ) /\ A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) ) )
63 62 simprd 
 |-  ( ( y u. u ) e. S -> A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) )
64 43 63 syl 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) )
65 simpll3 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> x e. y )
66 elun1 
 |-  ( x e. y -> x e. ( y u. u ) )
67 65 66 syl 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> x e. ( y u. u ) )
68 rsp 
 |-  ( A. x e. ( y u. u ) -. x e. ( N ` ( ( y u. u ) \ { x } ) ) -> ( x e. ( y u. u ) -> -. x e. ( N ` ( ( y u. u ) \ { x } ) ) ) )
69 64 67 68 sylc 
 |-  ( ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) /\ x e. ( N ` ( u \ { x } ) ) ) -> -. x e. ( N ` ( ( y u. u ) \ { x } ) ) )
70 53 69 pm2.65da 
 |-  ( ( ( ph /\ y e. A /\ x e. y ) /\ u e. A ) -> -. x e. ( N ` ( u \ { x } ) ) )
71 70 nrexdv 
 |-  ( ( ph /\ y e. A /\ x e. y ) -> -. E. u e. A x e. ( N ` ( u \ { x } ) ) )
72 1 2 3 4 5 6 7 8 9 10 11 12 lbsextlem2 
 |-  ( ph -> ( T e. P /\ ( U. A \ { x } ) C_ T ) )
73 72 simpld 
 |-  ( ph -> T e. P )
74 1 8 lssss 
 |-  ( T e. P -> T C_ V )
75 73 74 syl 
 |-  ( ph -> T C_ V )
76 72 simprd 
 |-  ( ph -> ( U. A \ { x } ) C_ T )
77 1 3 lspss 
 |-  ( ( W e. LMod /\ T C_ V /\ ( U. A \ { x } ) C_ T ) -> ( N ` ( U. A \ { x } ) ) C_ ( N ` T ) )
78 35 75 76 77 syl3anc 
 |-  ( ph -> ( N ` ( U. A \ { x } ) ) C_ ( N ` T ) )
79 8 3 lspid 
 |-  ( ( W e. LMod /\ T e. P ) -> ( N ` T ) = T )
80 35 73 79 syl2anc 
 |-  ( ph -> ( N ` T ) = T )
81 78 80 sseqtrd 
 |-  ( ph -> ( N ` ( U. A \ { x } ) ) C_ T )
82 81 3ad2ant1 
 |-  ( ( ph /\ y e. A /\ x e. y ) -> ( N ` ( U. A \ { x } ) ) C_ T )
83 82 12 sseqtrdi 
 |-  ( ( ph /\ y e. A /\ x e. y ) -> ( N ` ( U. A \ { x } ) ) C_ U_ u e. A ( N ` ( u \ { x } ) ) )
84 83 sseld 
 |-  ( ( ph /\ y e. A /\ x e. y ) -> ( x e. ( N ` ( U. A \ { x } ) ) -> x e. U_ u e. A ( N ` ( u \ { x } ) ) ) )
85 eliun 
 |-  ( x e. U_ u e. A ( N ` ( u \ { x } ) ) <-> E. u e. A x e. ( N ` ( u \ { x } ) ) )
86 84 85 imbitrdi 
 |-  ( ( ph /\ y e. A /\ x e. y ) -> ( x e. ( N ` ( U. A \ { x } ) ) -> E. u e. A x e. ( N ` ( u \ { x } ) ) ) )
87 71 86 mtod 
 |-  ( ( ph /\ y e. A /\ x e. y ) -> -. x e. ( N ` ( U. A \ { x } ) ) )
88 87 rexlimdv3a 
 |-  ( ph -> ( E. y e. A x e. y -> -. x e. ( N ` ( U. A \ { x } ) ) ) )
89 32 88 biimtrid 
 |-  ( ph -> ( x e. U. A -> -. x e. ( N ` ( U. A \ { x } ) ) ) )
90 89 ralrimiv 
 |-  ( ph -> A. x e. U. A -. x e. ( N ` ( U. A \ { x } ) ) )
91 31 90 jca 
 |-  ( ph -> ( C C_ U. A /\ A. x e. U. A -. x e. ( N ` ( U. A \ { x } ) ) ) )
92 sseq2 
 |-  ( z = U. A -> ( C C_ z <-> C C_ U. A ) )
93 difeq1 
 |-  ( z = U. A -> ( z \ { x } ) = ( U. A \ { x } ) )
94 93 fveq2d 
 |-  ( z = U. A -> ( N ` ( z \ { x } ) ) = ( N ` ( U. A \ { x } ) ) )
95 94 eleq2d 
 |-  ( z = U. A -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( U. A \ { x } ) ) ) )
96 95 notbid 
 |-  ( z = U. A -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( U. A \ { x } ) ) ) )
97 96 raleqbi1dv 
 |-  ( z = U. A -> ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. x e. U. A -. x e. ( N ` ( U. A \ { x } ) ) ) )
98 92 97 anbi12d 
 |-  ( z = U. A -> ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) <-> ( C C_ U. A /\ A. x e. U. A -. x e. ( N ` ( U. A \ { x } ) ) ) ) )
99 98 7 elrab2 
 |-  ( U. A e. S <-> ( U. A e. ~P V /\ ( C C_ U. A /\ A. x e. U. A -. x e. ( N ` ( U. A \ { x } ) ) ) ) )
100 19 91 99 sylanbrc 
 |-  ( ph -> U. A e. S )