Theorem lbsextlem4 17934

Description: Lemma for lbsext 17936. lbsextlem3 17933 satisfies the conditions for the application of Zorn's lemma zorn 8904 (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.)

Hypotheses

Ref	Expression
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

Ref	Expression
lbsextlem4	|- ( ph -> E. s e. J C C_ s )

Distinct variable groups:   x, J   ph, x, s   S, s, x   x, z, C   x, N, z   x, V, z   x, W   z, s   ph, s

Allowed substitution hints:   ph( z)   C( s)   S( z)   J( z, s)   N( s)   V( s)   W( z, s)

Proof of Theorem lbsextlem4

Dummy variables u w y t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lbsext.k	. . . 4 |- ( ph -> ~P V e. dom card )
2		lbsext.s	. . . . 5 |- S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
3		ssrab2 3581	. . . . 5 |- { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } C_ ~P V
4	2, 3	eqsstri 3529	. . . 4 |- S C_ ~P V
5		ssnum 8437	. . . 4 |- ( ( ~P V e. dom card /\ S C_ ~P V ) -> S e. dom card )
6	1, 4, 5	sylancl 662	. . 3 |- ( ph -> S e. dom card )
7		lbsext.v	. . . 4 |- V = ( Base ` W )
8		lbsext.j	. . . 4 |- J = (LBasis ` W )
9		lbsext.n	. . . 4 |- N = ( LSpan ` W )
10		lbsext.w	. . . 4 |- ( ph -> W e. LVec )
11		lbsext.c	. . . 4 |- ( ph -> C C_ V )
12		lbsext.x	. . . 4 |- ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
13	7, 8, 9, 10, 11, 12, 2	lbsextlem1 17931	. . 3 |- ( ph -> S =/= (/) )
14	10	adantr 465	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> W e. LVec )
15	11	adantr 465	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> C C_ V )
16	12	adantr 465	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
17		eqid 2457	. . . . . 6 |- ( LSubSp ` W ) = ( LSubSp ` W )
18		simpr1 1002	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y C_ S )
19		simpr2 1003	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y =/= (/) )
20		simpr3 1004	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> [ C.] Or y )
21		eqid 2457	. . . . . 6 |- U_ u e. y ( N ` ( u \ { x } ) ) = U_ u e. y ( N ` ( u \ { x } ) )
22	7, 8, 9, 14, 15, 16, 2, 17, 18, 19, 20, 21	lbsextlem3 17933	. . . . 5 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> U. y e. S )
23	22	ex 434	. . . 4 |- ( ph -> ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
24	23	alrimiv 1720	. . 3 |- ( ph -> A. y ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
25		zornn0g 8902	. . 3 |- ( ( 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 )
26	6, 13, 24, 25	syl3anc 1228	. 2 |- ( ph -> E. s e. S A. t e. S -. s C. t )
27		simprl 756	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. S )
28		sseq2 3521	. . . . . . . . . . 11 |- ( z = s -> ( C C_ z <-> C C_ s ) )
29		difeq1 3611	. . . . . . . . . . . . . . 15 |- ( z = s -> ( z \ { x } ) = ( s \ { x } ) )
30	29	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( z = s -> ( N ` ( z \ { x } ) ) = ( N ` ( s \ { x } ) ) )
31	30	eleq2d 2527	. . . . . . . . . . . . 13 |- ( z = s -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( s \ { x } ) ) ) )
32	31	notbid 294	. . . . . . . . . . . 12 |- ( z = s -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( s \ { x } ) ) ) )
33	32	raleqbi1dv 3062	. . . . . . . . . . 11 |- ( z = s -> ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) )
34	28, 33	anbi12d 710	. . . . . . . . . 10 |- ( 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 } ) ) ) ) )
35	34, 2	elrab2 3259	. . . . . . . . 9 |- ( s e. S <-> ( s e. ~P V /\ ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
36	27, 35	sylib 196	. . . . . . . 8 |- ( ( 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 } ) ) ) ) )
37	36	simpld 459	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. ~P V )
38	37	elpwid 4025	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ V )
39		lveclmod 17879	. . . . . . . . . 10 |- ( W e. LVec -> W e. LMod )
40	10, 39	syl 16	. . . . . . . . 9 |- ( ph -> W e. LMod )
41	40	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LMod )
42	7, 9	lspssv 17756	. . . . . . . 8 |- ( ( W e. LMod /\ s C_ V ) -> ( N ` s ) C_ V )
43	41, 38, 42	syl2anc 661	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) C_ V )
44		ssun1 3663	. . . . . . . . . . . 12 |- s C_ ( s u. { w } )
45	44	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ ( s u. { w } ) )
46		ssun2 3664	. . . . . . . . . . . . . 14 |- { w } C_ ( s u. { w } )
47		ssnid 4061	. . . . . . . . . . . . . 14 |- w e. { w }
48	46, 47	sselii 3496	. . . . . . . . . . . . 13 |- w e. ( s u. { w } )
49	7, 9	lspssid 17758	. . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ s C_ V ) -> s C_ ( N ` s ) )
50	41, 38, 49	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ ( N ` s ) )
51	50	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ ( N ` s ) )
52		eldifn 3623	. . . . . . . . . . . . . . 15 |- ( w e. ( V \ ( N ` s ) ) -> -. w e. ( N ` s ) )
53	52	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` s ) )
54	51, 53	ssneldd 3502	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. s )
55		nelne1 2786	. . . . . . . . . . . . 13 |- ( ( w e. ( s u. { w } ) /\ -. w e. s ) -> ( s u. { w } ) =/= s )
56	48, 54, 55	sylancr 663	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) =/= s )
57	56	necomd 2728	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s =/= ( s u. { w } ) )
58		df-pss 3487	. . . . . . . . . . 11 |- ( s C. ( s u. { w } ) <-> ( s C_ ( s u. { w } ) /\ s =/= ( s u. { w } ) ) )
59	45, 57, 58	sylanbrc 664	. . . . . . . . . 10 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C. ( s u. { w } ) )
60	38	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ V )
61		eldifi 3622	. . . . . . . . . . . . . . . 16 |- ( w e. ( V \ ( N ` s ) ) -> w e. V )
62	61	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> w e. V )
63	62	snssd 4177	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> { w } C_ V )
64	60, 63	unssd 3676	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) C_ V )
65		fvex 5882	. . . . . . . . . . . . . . 15 |- ( Base ` W ) e. _V
66	7, 65	eqeltri 2541	. . . . . . . . . . . . . 14 |- V e. _V
67	66	elpw2 4620	. . . . . . . . . . . . 13 |- ( ( s u. { w } ) e. ~P V <-> ( s u. { w } ) C_ V )
68	64, 67	sylibr 212	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. ~P V )
69	36	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) )
70	69	simpld 459	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> C C_ s )
71	70	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ s )
72	71, 44	syl6ss 3511	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ ( s u. { w } ) )
73	10	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 )
74	38	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 )
75	74	ssdifssd 3638	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 )
76	62	adantrr 716	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 )
77		simprrr 766	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 } ) ) )
78		simprrl 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( 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 )
79	54	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( 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 )
80		nelne2 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. s /\ -. w e. s ) -> x =/= w )
81	78, 79, 80	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( 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 )
82		elsni 4057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. { w } -> x = w )
83	82	necon3ai 2685	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x =/= w -> -. x e. { w } )
84	81, 83	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( 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 } )
85		disjsn 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { w } i^i { x } ) = (/) <-> -. x e. { w } )
86	84, 85	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 } ) = (/) )
87		disj3 3874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( { w } i^i { x } ) = (/) <-> { w } = ( { w } \ { x } ) )
88	86, 87	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 } ) )
89	88	uneq2d 3654	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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 } ) ) )
90		difundir 3758	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) )
91	89, 90	syl6reqr 2517	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 5876	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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	77, 92	eleqtrd 2547	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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	69	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> A. x e. s -. x e. ( N ` ( s \ { x } ) ) )
95	94	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 2823	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. x e. s -. x e. ( N ` ( s \ { x } ) ) -> ( x e. s -> -. x e. ( N ` ( s \ { x } ) ) ) )
97	95, 78, 96	sylc 60	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 3482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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	7, 17, 9	lspsolv 17916	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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	73, 75, 76, 98, 99	syl13anc 1230	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 3906	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s \ { x } ) u. { x } ) = ( s u. { x } )
102	78	snssd 4177	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 3673	. . . . . . . . . . . . . . . . . . . . . 22 |- ( { x } C_ s <-> ( s u. { x } ) = s )
104	102, 103	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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	syl5eq 2510	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 5876	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 2547	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 615	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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	53, 108	mtod 177	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 422	. . . . . . . . . . . . . . . 16 |- ( ( x e. s -> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) <-> -. ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
111	109, 110	sylibr 212	. . . . . . . . . . . . . . 15 |- ( ( ( 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 2869	. . . . . . . . . . . . . 14 |- ( ( ( 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 3628	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s \ { w } ) C_ s )
114	7, 9	lspss 17757	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. LMod /\ s C_ V /\ ( s \ { w } ) C_ s ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
115	41, 38, 113, 114	syl3anc 1228	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
116	115	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
117	116, 53	ssneldd 3502	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` ( s \ { w } ) ) )
118		vex 3112	. . . . . . . . . . . . . . . 16 |- w e. _V
119		id 22	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> x = w )
120		sneq 4042	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = w -> { x } = { w } )
121	120	difeq2d 3618	. . . . . . . . . . . . . . . . . . . 20 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( ( s u. { w } ) \ { w } ) )
122		difun2 3910	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s u. { w } ) \ { w } ) = ( s \ { w } )
123	121, 122	syl6eq 2514	. . . . . . . . . . . . . . . . . . 19 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( s \ { w } ) )
124	123	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( s \ { w } ) ) )
125	119, 124	eleq12d 2539	. . . . . . . . . . . . . . . . 17 |- ( x = w -> ( x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> w e. ( N ` ( s \ { w } ) ) ) )
126	125	notbid 294	. . . . . . . . . . . . . . . 16 |- ( x = w -> ( -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) ) )
127	118, 126	ralsn 4071	. . . . . . . . . . . . . . 15 |- ( A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) )
128	117, 127	sylibr 212	. . . . . . . . . . . . . 14 |- ( ( ( 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 3682	. . . . . . . . . . . . . 14 |- ( ( 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 661	. . . . . . . . . . . . 13 |- ( ( ( 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	72, 130	jca 532	. . . . . . . . . . . 12 |- ( ( ( 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 3521	. . . . . . . . . . . . . 14 |- ( z = ( s u. { w } ) -> ( C C_ z <-> C C_ ( s u. { w } ) ) )
133		difeq1 3611	. . . . . . . . . . . . . . . . . 18 |- ( z = ( s u. { w } ) -> ( z \ { x } ) = ( ( s u. { w } ) \ { x } ) )
134	133	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( z = ( s u. { w } ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( s u. { w } ) \ { x } ) ) )
135	134	eleq2d 2527	. . . . . . . . . . . . . . . 16 |- ( z = ( s u. { w } ) -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
136	135	notbid 294	. . . . . . . . . . . . . . 15 |- ( z = ( s u. { w } ) -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
137	136	raleqbi1dv 3062	. . . . . . . . . . . . . 14 |- ( 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 710	. . . . . . . . . . . . 13 |- ( 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, 2	elrab2 3259	. . . . . . . . . . . 12 |- ( ( 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	68, 131, 139	sylanbrc 664	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. S )
141		simplrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> A. t e. S -. s C. t )
142		psseq2 3588	. . . . . . . . . . . . 13 |- ( t = ( s u. { w } ) -> ( s C. t <-> s C. ( s u. { w } ) ) )
143	142	notbid 294	. . . . . . . . . . . 12 |- ( t = ( s u. { w } ) -> ( -. s C. t <-> -. s C. ( s u. { w } ) ) )
144	143	rspcv 3206	. . . . . . . . . . 11 |- ( ( s u. { w } ) e. S -> ( A. t e. S -. s C. t -> -. s C. ( s u. { w } ) ) )
145	140, 141, 144	sylc 60	. . . . . . . . . 10 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. s C. ( s u. { w } ) )
146	59, 145	pm2.65da 576	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> -. w e. ( V \ ( N ` s ) ) )
147	146	eq0rdv 3829	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( V \ ( N ` s ) ) = (/) )
148		ssdif0 3888	. . . . . . . 8 |- ( V C_ ( N ` s ) <-> ( V \ ( N ` s ) ) = (/) )
149	147, 148	sylibr 212	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> V C_ ( N ` s ) )
150	43, 149	eqssd 3516	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) = V )
151	10	adantr 465	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LVec )
152	7, 8, 9	islbs2 17927	. . . . . . 7 |- ( W e. LVec -> ( s e. J <-> ( s C_ V /\ ( N ` s ) = V /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
153	151, 152	syl 16	. . . . . 6 |- ( ( 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 } ) ) ) ) )
154	38, 150, 94, 153	mpbir3and 1179	. . . . 5 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. J )
155	154, 70	jca 532	. . . 4 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s e. J /\ C C_ s ) )
156	155	ex 434	. . 3 |- ( ph -> ( ( s e. S /\ A. t e. S -. s C. t ) -> ( s e. J /\ C C_ s ) ) )
157	156	reximdv2 2928	. 2 |- ( ph -> ( E. s e. S A. t e. S -. s C. t -> E. s e. J C C_ s ) )
158	26, 157	mpd 15	1 |- ( ph -> E. s e. J C C_ s )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   A.wal 1393   = wceq 1395   e. wcel 1819   =/= wne 2652   A.wral 2807   E.wrex 2808   {crab 2811   _Vcvv 3109   \ cdif 3468   u. cun 3469   i^i cin 3470   C_ wss 3471   C. wpss 3472   (/)c0 3793   ~Pcpw 4015   {csn 4032   U.cuni 4251   U_ciun 4332   Or wor 4808   dom cdm 5008   ` cfv 5594   [ C.] crpss 6578   cardccrd 8333   Basecbs 14644   LModclmod 17639   LSubSpclss 17705   LSpanclspn 17744  LBasisclbs 17847   LVecclvec 17875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-rpss 6579  df-om 6700  df-1st 6799  df-2nd 6800  df-tpos 6973  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-3 10616  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-0g 14859  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-grp 16184  df-minusg 16185  df-sbg 16186  df-cmn 16927  df-abl 16928  df-mgp 17269  df-ur 17281  df-ring 17327  df-oppr 17399  df-dvdsr 17417  df-unit 17418  df-invr 17448  df-drng 17525  df-lmod 17641  df-lss 17706  df-lsp 17745  df-lbs 17848  df-lvec 17876

This theorem is referenced by:  lbsextg  17935