Theorem lbsextlem4 16188

Description: Lemma for lbsext 16190. lbsextlem3 16187 satisfies the conditions for the application of Zorn's lemma zorn 8343 (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 3388	. . . . 5 |- { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } C_ ~P V
4	2, 3	eqsstri 3338	. . . 4 |- S C_ ~P V
5		ssnum 7876	. . . 4 |- ( ( ~P V e. dom card /\ S C_ ~P V ) -> S e. dom card )
6	1, 4, 5	sylancl 644	. . 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 16185	. . 3 |- ( ph -> S =/= (/) )
14	10	adantr 452	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> W e. LVec )
15	11	adantr 452	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> C C_ V )
16	12	adantr 452	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
17		eqid 2404	. . . . . 6 |- ( LSubSp ` W ) = ( LSubSp ` W )
18		simpr1 963	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y C_ S )
19		simpr2 964	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y =/= (/) )
20		simpr3 965	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> [ C.] Or y )
21		eqid 2404	. . . . . 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 16187	. . . . 5 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> U. y e. S )
23	22	ex 424	. . . 4 |- ( ph -> ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
24	23	alrimiv 1638	. . 3 |- ( ph -> A. y ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
25		zornn0g 8341	. . 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 1184	. 2 |- ( ph -> E. s e. S A. t e. S -. s C. t )
27		simprl 733	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. S )
28		sseq2 3330	. . . . . . . . . . 11 |- ( z = s -> ( C C_ z <-> C C_ s ) )
29		difeq1 3418	. . . . . . . . . . . . . . 15 |- ( z = s -> ( z \ { x } ) = ( s \ { x } ) )
30	29	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( z = s -> ( N ` ( z \ { x } ) ) = ( N ` ( s \ { x } ) ) )
31	30	eleq2d 2471	. . . . . . . . . . . . 13 |- ( z = s -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( s \ { x } ) ) ) )
32	31	notbid 286	. . . . . . . . . . . 12 |- ( z = s -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( s \ { x } ) ) ) )
33	32	raleqbi1dv 2872	. . . . . . . . . . 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 692	. . . . . . . . . 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 3054	. . . . . . . . 9 |- ( s e. S <-> ( s e. ~P V /\ ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
36	27, 35	sylib 189	. . . . . . . 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 446	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. ~P V )
38	37	elpwid 3768	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ V )
39		lveclmod 16133	. . . . . . . . . 10 |- ( W e. LVec -> W e. LMod )
40	10, 39	syl 16	. . . . . . . . 9 |- ( ph -> W e. LMod )
41	40	adantr 452	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LMod )
42	7, 9	lspssv 16014	. . . . . . . 8 |- ( ( W e. LMod /\ s C_ V ) -> ( N ` s ) C_ V )
43	41, 38, 42	syl2anc 643	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) C_ V )
44		ssun1 3470	. . . . . . . . . . . 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 3471	. . . . . . . . . . . . . 14 |- { w } C_ ( s u. { w } )
47		vex 2919	. . . . . . . . . . . . . . 15 |- w e. _V
48	47	snid 3801	. . . . . . . . . . . . . 14 |- w e. { w }
49	46, 48	sselii 3305	. . . . . . . . . . . . 13 |- w e. ( s u. { w } )
50	7, 9	lspssid 16016	. . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ s C_ V ) -> s C_ ( N ` s ) )
51	41, 38, 50	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ ( N ` s ) )
52	51	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ ( N ` s ) )
53		eldifn 3430	. . . . . . . . . . . . . . 15 |- ( w e. ( V \ ( N ` s ) ) -> -. w e. ( N ` s ) )
54	53	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` s ) )
55	52, 54	ssneldd 3311	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. s )
56		nelne1 2656	. . . . . . . . . . . . 13 |- ( ( w e. ( s u. { w } ) /\ -. w e. s ) -> ( s u. { w } ) =/= s )
57	49, 55, 56	sylancr 645	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) =/= s )
58	57	necomd 2650	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s =/= ( s u. { w } ) )
59		df-pss 3296	. . . . . . . . . . 11 |- ( s C. ( s u. { w } ) <-> ( s C_ ( s u. { w } ) /\ s =/= ( s u. { w } ) ) )
60	45, 58, 59	sylanbrc 646	. . . . . . . . . 10 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C. ( s u. { w } ) )
61	38	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s C_ V )
62		eldifi 3429	. . . . . . . . . . . . . . . 16 |- ( w e. ( V \ ( N ` s ) ) -> w e. V )
63	62	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> w e. V )
64	63	snssd 3903	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> { w } C_ V )
65	61, 64	unssd 3483	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) C_ V )
66		fvex 5701	. . . . . . . . . . . . . . 15 |- ( Base ` W ) e. _V
67	7, 66	eqeltri 2474	. . . . . . . . . . . . . 14 |- V e. _V
68	67	elpw2 4324	. . . . . . . . . . . . 13 |- ( ( s u. { w } ) e. ~P V <-> ( s u. { w } ) C_ V )
69	65, 68	sylibr 204	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. ~P V )
70	36	simprd 450	. . . . . . . . . . . . . . . 16 |- ( ( 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 446	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> C C_ s )
72	71	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ s )
73	72, 44	syl6ss 3320	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> C C_ ( s u. { w } ) )
74	10	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 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 )
75	38	adantr 452	. . . . . . . . . . . . . . . . . . . . 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 )
76	75	ssdifssd 3445	. . . . . . . . . . . . . . . . . . . 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 )
77	63	adantrr 698	. . . . . . . . . . . . . . . . . . . 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 )
78		simprrr 742	. . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
79		simprrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
80	55	adantrr 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
81		nelne2 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. s /\ -. w e. s ) -> x =/= w )
82	79, 80, 81	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
83		elsni 3798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. { w } -> x = w )
84	83	necon3ai 2607	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x =/= w -> -. x e. { w } )
85	82, 84	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 } )
86		disjsn 3828	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { w } i^i { x } ) = (/) <-> -. x e. { w } )
87	85, 86	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) = (/) )
88		disj3 3632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( { w } i^i { x } ) = (/) <-> { w } = ( { w } \ { x } ) )
89	87, 88	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
90	89	uneq2d 3461	. . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
91		difundir 3554	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) )
92	90, 91	syl6reqr 2455	. . . . . . . . . . . . . . . . . . . . . . 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 } ) )
93	92	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
94	78, 93	eleqtrd 2480	. . . . . . . . . . . . . . . . . . . . 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 } ) ) )
95	70	simprd 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> A. x e. s -. x e. ( N ` ( s \ { x } ) ) )
96	95	adantr 452	. . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
97		rsp 2726	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. x e. s -. x e. ( N ` ( s \ { x } ) ) -> ( x e. s -> -. x e. ( N ` ( s \ { x } ) ) ) )
98	96, 79, 97	sylc 58	. . . . . . . . . . . . . . . . . . . . 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 } ) ) )
99	94, 98	eldifd 3291	. . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
100	7, 17, 9	lspsolv 16170	. . . . . . . . . . . . . . . . . . . 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 } ) ) )
101	74, 76, 77, 99, 100	syl13anc 1186	. . . . . . . . . . . . . . . . . . 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 } ) ) )
102		undif1 3663	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s \ { x } ) u. { x } ) = ( s u. { x } )
103	79	snssd 3903	. . . . . . . . . . . . . . . . . . . . . 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 )
104		ssequn2 3480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( { x } C_ s <-> ( s u. { x } ) = s )
105	103, 104	sylib 189	. . . . . . . . . . . . . . . . . . . . 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 )
106	102, 105	syl5eq 2448	. . . . . . . . . . . . . . . . . . . 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 )
107	106	fveq2d 5691	. . . . . . . . . . . . . . . . . . 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 ) )
108	101, 107	eleqtrd 2480	. . . . . . . . . . . . . . . . . 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 ) )
109	108	expr 599	. . . . . . . . . . . . . . . . 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 ) ) )
110	54, 109	mtod 170	. . . . . . . . . . . . . . . 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 } ) ) ) )
111		imnan 412	. . . . . . . . . . . . . . . 16 |- ( ( x e. s -> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) <-> -. ( x e. s /\ x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
112	110, 111	sylibr 204	. . . . . . . . . . . . . . 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 } ) ) ) )
113	112	ralrimiv 2748	. . . . . . . . . . . . . 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 } ) ) )
114		difssd 3435	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s \ { w } ) C_ s )
115	7, 9	lspss 16015	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. LMod /\ s C_ V /\ ( s \ { w } ) C_ s ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
116	41, 38, 114, 115	syl3anc 1184	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
117	116	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
118	117, 54	ssneldd 3311	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` ( s \ { w } ) ) )
119		id 20	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> x = w )
120		sneq 3785	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = w -> { x } = { w } )
121	120	difeq2d 3425	. . . . . . . . . . . . . . . . . . . 20 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( ( s u. { w } ) \ { w } ) )
122		difun2 3667	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s u. { w } ) \ { w } ) = ( s \ { w } )
123	121, 122	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( s \ { w } ) )
124	123	fveq2d 5691	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( s \ { w } ) ) )
125	119, 124	eleq12d 2472	. . . . . . . . . . . . . . . . 17 |- ( x = w -> ( x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> w e. ( N ` ( s \ { w } ) ) ) )
126	125	notbid 286	. . . . . . . . . . . . . . . 16 |- ( x = w -> ( -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) ) )
127	47, 126	ralsn 3809	. . . . . . . . . . . . . . 15 |- ( A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) )
128	118, 127	sylibr 204	. . . . . . . . . . . . . 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 3489	. . . . . . . . . . . . . 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	113, 128, 129	syl2anc 643	. . . . . . . . . . . . 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	73, 130	jca 519	. . . . . . . . . . . 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 3330	. . . . . . . . . . . . . 14 |- ( z = ( s u. { w } ) -> ( C C_ z <-> C C_ ( s u. { w } ) ) )
133		difeq1 3418	. . . . . . . . . . . . . . . . . 18 |- ( z = ( s u. { w } ) -> ( z \ { x } ) = ( ( s u. { w } ) \ { x } ) )
134	133	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( z = ( s u. { w } ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( s u. { w } ) \ { x } ) ) )
135	134	eleq2d 2471	. . . . . . . . . . . . . . . 16 |- ( z = ( s u. { w } ) -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
136	135	notbid 286	. . . . . . . . . . . . . . 15 |- ( z = ( s u. { w } ) -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) ) )
137	136	raleqbi1dv 2872	. . . . . . . . . . . . . 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 692	. . . . . . . . . . . . 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 3054	. . . . . . . . . . . 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	69, 131, 139	sylanbrc 646	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) e. S )
141		simplrr 738	. . . . . . . . . . 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 3395	. . . . . . . . . . . . 13 |- ( t = ( s u. { w } ) -> ( s C. t <-> s C. ( s u. { w } ) ) )
143	142	notbid 286	. . . . . . . . . . . 12 |- ( t = ( s u. { w } ) -> ( -. s C. t <-> -. s C. ( s u. { w } ) ) )
144	143	rspcv 3008	. . . . . . . . . . 11 |- ( ( s u. { w } ) e. S -> ( A. t e. S -. s C. t -> -. s C. ( s u. { w } ) ) )
145	140, 141, 144	sylc 58	. . . . . . . . . 10 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. s C. ( s u. { w } ) )
146	60, 145	pm2.65da 560	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> -. w e. ( V \ ( N ` s ) ) )
147	146	eq0rdv 3622	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( V \ ( N ` s ) ) = (/) )
148		ssdif0 3646	. . . . . . . 8 |- ( V C_ ( N ` s ) <-> ( V \ ( N ` s ) ) = (/) )
149	147, 148	sylibr 204	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> V C_ ( N ` s ) )
150	43, 149	eqssd 3325	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( N ` s ) = V )
151	10	adantr 452	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> W e. LVec )
152	7, 8, 9	islbs2 16181	. . . . . . 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, 95, 153	mpbir3and 1137	. . . . 5 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. J )
155	154, 71	jca 519	. . . 4 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s e. J /\ C C_ s ) )
156	155	ex 424	. . 3 |- ( ph -> ( ( s e. S /\ A. t e. S -. s C. t ) -> ( s e. J /\ C C_ s ) ) )
157	156	reximdv2 2775	. 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 177   /\ wa 359   /\ w3a 936   A.wal 1546   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   C. wpss 3281   (/)c0 3588   ~Pcpw 3759   {csn 3774   U.cuni 3975   U_ciun 4053   Or wor 4462   dom cdm 4837   ` cfv 5413   [ C.] crpss 6480   cardccrd 7778   Basecbs 13424   LModclmod 15905   LSubSpclss 15963   LSpanclspn 16002  LBasisclbs 16101   LVecclvec 16129

This theorem is referenced by:  lbsextg  16189

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-tpos 6438  df-rpss 6481  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-0g 13682  df-mnd 14645  df-grp 14767  df-minusg 14768  df-sbg 14769  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-ur 15620  df-oppr 15683  df-dvdsr 15701  df-unit 15702  df-invr 15732  df-drng 15792  df-lmod 15907  df-lss 15964  df-lsp 16003  df-lbs 16102  df-lvec 16130