Theorem lbsextlem4 18369

Description: Lemma for lbsext 18371. lbsextlem3 18368 satisfies the conditions for the application of Zorn's lemma zorn 8937 (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 3546	. . . . 5 |- { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } C_ ~P V
4	2, 3	eqsstri 3494	. . . 4 |- S C_ ~P V
5		ssnum 8470	. . . 4 |- ( ( ~P V e. dom card /\ S C_ ~P V ) -> S e. dom card )
6	1, 4, 5	sylancl 666	. . 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 18366	. . 3 |- ( ph -> S =/= (/) )
14	10	adantr 466	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> W e. LVec )
15	11	adantr 466	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> C C_ V )
16	12	adantr 466	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
17		eqid 2422	. . . . . 6 |- ( LSubSp ` W ) = ( LSubSp ` W )
18		simpr1 1011	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y C_ S )
19		simpr2 1012	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y =/= (/) )
20		simpr3 1013	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> [ C.] Or y )
21		eqid 2422	. . . . . 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 18368	. . . . 5 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> U. y e. S )
23	22	ex 435	. . . 4 |- ( ph -> ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
24	23	alrimiv 1763	. . 3 |- ( ph -> A. y ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
25		zornn0g 8935	. . 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 1264	. 2 |- ( ph -> E. s e. S A. t e. S -. s C. t )
27		simprl 762	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. S )
28		sseq2 3486	. . . . . . . . . . 11 |- ( z = s -> ( C C_ z <-> C C_ s ) )
29		difeq1 3576	. . . . . . . . . . . . . . 15 |- ( z = s -> ( z \ { x } ) = ( s \ { x } ) )
30	29	fveq2d 5881	. . . . . . . . . . . . . 14 |- ( z = s -> ( N ` ( z \ { x } ) ) = ( N ` ( s \ { x } ) ) )
31	30	eleq2d 2492	. . . . . . . . . . . . 13 |- ( z = s -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( s \ { x } ) ) ) )
32	31	notbid 295	. . . . . . . . . . . 12 |- ( z = s -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( s \ { x } ) ) ) )
33	32	raleqbi1dv 3033	. . . . . . . . . . 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 715	. . . . . . . . . 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 3231	. . . . . . . . 9 |- ( s e. S <-> ( s e. ~P V /\ ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
36	27, 35	sylib 199	. . . . . . . 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 460	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. ~P V )
38	37	elpwid 3989	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ V )
39		lveclmod 18314	. . . . . . . . . 10 |- ( W e. LVec -> W e. LMod )
40	10, 39	syl 17	. . . . . . . . 9 |- ( ph -> W e. LMod )
41	40	adantr 466	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LMod )
42	7, 9	lspssv 18191	. . . . . . . 8 |- ( ( W e. LMod /\ s C_ V ) -> ( N ` s ) C_ V )
43	41, 38, 42	syl2anc 665	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) C_ V )
44		ssun1 3629	. . . . . . . . . . . 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 3630	. . . . . . . . . . . . . 14 |- { w } C_ ( s u. { w } )
47		ssnid 4025	. . . . . . . . . . . . . 14 |- w e. { w }
48	46, 47	sselii 3461	. . . . . . . . . . . . 13 |- w e. ( s u. { w } )
49	7, 9	lspssid 18193	. . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ s C_ V ) -> s C_ ( N ` s ) )
50	41, 38, 49	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ ( N ` s ) )
51	50	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ ( N ` s ) )
52		eldifn 3588	. . . . . . . . . . . . . . 15 |- ( w e. ( V \ ( N ` s ) ) -> -. w e. ( N ` s ) )
53	52	adantl 467	. . . . . . . . . . . . . 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 3467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. s )
55		nelne1 2753	. . . . . . . . . . . . 13 |- ( ( w e. ( s u. { w } ) /\ -. w e. s ) -> ( s u. { w } ) =/= s )
56	48, 54, 55	sylancr 667	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) =/= s )
57	56	necomd 2695	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s =/= ( s u. { w } ) )
58		df-pss 3452	. . . . . . . . . . 11 |- ( s C. ( s u. { w } ) <-> ( s C_ ( s u. { w } ) /\ s =/= ( s u. { w } ) ) )
59	45, 57, 58	sylanbrc 668	. . . . . . . . . 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 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ V )
61		eldifi 3587	. . . . . . . . . . . . . . . 16 |- ( w e. ( V \ ( N ` s ) ) -> w e. V )
62	61	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> w e. V )
63	62	snssd 4142	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> { w } C_ V )
64	60, 63	unssd 3642	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) C_ V )
65		fvex 5887	. . . . . . . . . . . . . . 15 |- ( Base ` W ) e. _V
66	7, 65	eqeltri 2506	. . . . . . . . . . . . . 14 |- V e. _V
67	66	elpw2 4584	. . . . . . . . . . . . 13 |- ( ( s u. { w } ) e. ~P V <-> ( s u. { w } ) C_ V )
68	64, 67	sylibr 215	. . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> C C_ s )
71	70	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ s )
72	71, 44	syl6ss 3476	. . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . 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 3603	. . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. s /\ -. w e. s ) -> x =/= w )
81	78, 79, 80	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. { w } -> x = w )
83	82	necon3ai 2652	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x =/= w -> -. x e. { w } )
84	81, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 4057	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { w } i^i { x } ) = (/) <-> -. x e. { w } )
86	84, 85	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3837	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( { w } i^i { x } ) = (/) <-> { w } = ( { w } \ { x } ) )
88	86, 87	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . 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 3620	. . . . . . . . . . . . . . . . . . . . . . . 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 3726	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) )
91	89, 90	syl6reqr 2482	. . . . . . . . . . . . . . . . . . . . . . 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 5881	. . . . . . . . . . . . . . . . . . . . . 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 2512	. . . . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> A. x e. s -. x e. ( N ` ( s \ { x } ) ) )
95	94	adantr 466	. . . . . . . . . . . . . . . . . . . . . 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 2791	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. x e. s -. x e. ( N ` ( s \ { x } ) ) -> ( x e. s -> -. x e. ( N ` ( s \ { x } ) ) ) )
97	95, 78, 96	sylc 62	. . . . . . . . . . . . . . . . . . . . 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 3447	. . . . . . . . . . . . . . . . . . . 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 18351	. . . . . . . . . . . . . . . . . . . 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 1266	. . . . . . . . . . . . . . . . . . 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 3870	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s \ { x } ) u. { x } ) = ( s u. { x } )
102	78	snssd 4142	. . . . . . . . . . . . . . . . . . . . . 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 3639	. . . . . . . . . . . . . . . . . . . . . 22 |- ( { x } C_ s <-> ( s u. { x } ) = s )
104	102, 103	sylib 199	. . . . . . . . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . . . . . . . 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 5881	. . . . . . . . . . . . . . . . . . 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 2512	. . . . . . . . . . . . . . . . . 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 618	. . . . . . . . . . . . . . . . 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 180	. . . . . . . . . . . . . . . 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 423	. . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . 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 3593	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s \ { w } ) C_ s )
114	7, 9	lspss 18192	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. LMod /\ s C_ V /\ ( s \ { w } ) C_ s ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
115	41, 38, 113, 114	syl3anc 1264	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
116	115	adantr 466	. . . . . . . . . . . . . . . 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 3467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` ( s \ { w } ) ) )
118		vex 3084	. . . . . . . . . . . . . . . 16 |- w e. _V
119		id 23	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> x = w )
120		sneq 4006	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = w -> { x } = { w } )
121	120	difeq2d 3583	. . . . . . . . . . . . . . . . . . . 20 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( ( s u. { w } ) \ { w } ) )
122		difun2 3875	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s u. { w } ) \ { w } ) = ( s \ { w } )
123	121, 122	syl6eq 2479	. . . . . . . . . . . . . . . . . . 19 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( s \ { w } ) )
124	123	fveq2d 5881	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( s \ { w } ) ) )
125	119, 124	eleq12d 2504	. . . . . . . . . . . . . . . . 17 |- ( x = w -> ( x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> w e. ( N ` ( s \ { w } ) ) ) )
126	125	notbid 295	. . . . . . . . . . . . . . . 16 |- ( x = w -> ( -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) ) )
127	118, 126	ralsn 4035	. . . . . . . . . . . . . . 15 |- ( A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) )
128	117, 127	sylibr 215	. . . . . . . . . . . . . 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 3648	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 534	. . . . . . . . . . . 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 3486	. . . . . . . . . . . . . 14 |- ( z = ( s u. { w } ) -> ( C C_ z <-> C C_ ( s u. { w } ) ) )
133		difeq1 3576	. . . . . . . . . . . . . . . . . 18 |- ( z = ( s u. { w } ) -> ( z \ { x } ) = ( ( s u. { w } ) \ { x } ) )
134	133	fveq2d 5881	. . . . . . . . . . . . . . . . 17 |- ( z = ( s u. { w } ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( s u. { w } ) \ { x } ) ) )
135	134	eleq2d 2492	. . . . . . . . . . . . . . . 16 |- ( z = ( s u. { w } ) -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
136	135	notbid 295	. . . . . . . . . . . . . . 15 |- ( z = ( s u. { w } ) -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
137	136	raleqbi1dv 3033	. . . . . . . . . . . . . 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 715	. . . . . . . . . . . . 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 3231	. . . . . . . . . . . 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 668	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. S )
141		simplrr 769	. . . . . . . . . . 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 3553	. . . . . . . . . . . . 13 |- ( t = ( s u. { w } ) -> ( s C. t <-> s C. ( s u. { w } ) ) )
143	142	notbid 295	. . . . . . . . . . . 12 |- ( t = ( s u. { w } ) -> ( -. s C. t <-> -. s C. ( s u. { w } ) ) )
144	143	rspcv 3178	. . . . . . . . . . 11 |- ( ( s u. { w } ) e. S -> ( A. t e. S -. s C. t -> -. s C. ( s u. { w } ) ) )
145	140, 141, 144	sylc 62	. . . . . . . . . 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 578	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> -. w e. ( V \ ( N ` s ) ) )
147	146	eq0rdv 3797	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( V \ ( N ` s ) ) = (/) )
148		ssdif0 3851	. . . . . . . 8 |- ( V C_ ( N ` s ) <-> ( V \ ( N ` s ) ) = (/) )
149	147, 148	sylibr 215	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> V C_ ( N ` s ) )
150	43, 149	eqssd 3481	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) = V )
151	10	adantr 466	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LVec )
152	7, 8, 9	islbs2 18362	. . . . . . 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 17	. . . . . 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 1188	. . . . 5 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. J )
155	154, 70	jca 534	. . . 4 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s e. J /\ C C_ s ) )
156	155	ex 435	. . 3 |- ( ph -> ( ( s e. S /\ A. t e. S -. s C. t ) -> ( s e. J /\ C C_ s ) ) )
157	156	reximdv2 2896	. 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 187   /\ wa 370   /\ w3a 982   A.wal 1435   = wceq 1437   e. wcel 1868   =/= wne 2618   A.wral 2775   E.wrex 2776   {crab 2779   _Vcvv 3081   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   C. wpss 3437   (/)c0 3761   ~Pcpw 3979   {csn 3996   U.cuni 4216   U_ciun 4296   Or wor 4769   dom cdm 4849   ` cfv 5597   [ C.] crpss 6580   cardccrd 8370   Basecbs 15106   LModclmod 18076   LSubSpclss 18140   LSpanclspn 18179  LBasisclbs 18282   LVecclvec 18310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-rpss 6581  df-om 6703  df-1st 6803  df-2nd 6804  df-tpos 6977  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-oadd 7190  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-3 10669  df-ndx 15109  df-slot 15110  df-base 15111  df-sets 15112  df-ress 15113  df-plusg 15188  df-mulr 15189  df-0g 15325  df-mgm 16473  df-sgrp 16512  df-mnd 16522  df-grp 16658  df-minusg 16659  df-sbg 16660  df-cmn 17417  df-abl 17418  df-mgp 17709  df-ur 17721  df-ring 17767  df-oppr 17836  df-dvdsr 17854  df-unit 17855  df-invr 17885  df-drng 17962  df-lmod 18078  df-lss 18141  df-lsp 18180  df-lbs 18283  df-lvec 18311

This theorem is referenced by:  lbsextg  18370