Theorem lbsextlem4 17602

Description: Lemma for lbsext 17604. lbsextlem3 17601 satisfies the conditions for the application of Zorn's lemma zorn 8886 (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 3585	. . . . 5 |- { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } C_ ~P V
4	2, 3	eqsstri 3534	. . . 4 |- S C_ ~P V
5		ssnum 8419	. . . 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 17599	. . 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 2467	. . . . . 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 2467	. . . . . 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 17601	. . . . 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 1695	. . 3 |- ( ph -> A. y ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
25		zornn0g 8884	. . 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 755	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. S )
28		sseq2 3526	. . . . . . . . . . 11 |- ( z = s -> ( C C_ z <-> C C_ s ) )
29		difeq1 3615	. . . . . . . . . . . . . . 15 |- ( z = s -> ( z \ { x } ) = ( s \ { x } ) )
30	29	fveq2d 5869	. . . . . . . . . . . . . 14 |- ( z = s -> ( N ` ( z \ { x } ) ) = ( N ` ( s \ { x } ) ) )
31	30	eleq2d 2537	. . . . . . . . . . . . 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 3066	. . . . . . . . . . 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 3263	. . . . . . . . 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 4020	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ V )
39		lveclmod 17547	. . . . . . . . . 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 17424	. . . . . . . 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 3667	. . . . . . . . . . . 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 3668	. . . . . . . . . . . . . 14 |- { w } C_ ( s u. { w } )
47		ssnid 4056	. . . . . . . . . . . . . 14 |- w e. { w }
48	46, 47	sselii 3501	. . . . . . . . . . . . 13 |- w e. ( s u. { w } )
49	7, 9	lspssid 17426	. . . . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . . 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 3507	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. s )
55		nelne1 2796	. . . . . . . . . . . . 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 2738	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s =/= ( s u. { w } ) )
58		df-pss 3492	. . . . . . . . . . 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 3626	. . . . . . . . . . . . . . . 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 4172	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> { w } C_ V )
64	60, 63	unssd 3680	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) C_ V )
65		fvex 5875	. . . . . . . . . . . . . . 15 |- ( Base ` W ) e. _V
66	7, 65	eqeltri 2551	. . . . . . . . . . . . . 14 |- V e. _V
67	66	elpw2 4611	. . . . . . . . . . . . 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 3516	. . . . . . . . . . . . 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 3642	. . . . . . . . . . . . . . . . . . . 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 764	. . . . . . . . . . . . . . . . . . . . . 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 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. { w } -> x = w )
83	82	necon3ai 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4088	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3871	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3658	. . . . . . . . . . . . . . . . . . . . . . . 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 3751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) )
91	89, 90	syl6reqr 2527	. . . . . . . . . . . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . . . . . . . . . . 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 2557	. . . . . . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . . . . . . . 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 3487	. . . . . . . . . . . . . . . . . . . 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 17584	. . . . . . . . . . . . . . . . . . . 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 3902	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s \ { x } ) u. { x } ) = ( s u. { x } )
102	78	snssd 4172	. . . . . . . . . . . . . . . . . . . . . 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 3677	. . . . . . . . . . . . . . . . . . . . . 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 2520	. . . . . . . . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . . . . . . . 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 2557	. . . . . . . . . . . . . . . . . 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 2876	. . . . . . . . . . . . . 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 3632	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s \ { w } ) C_ s )
114	7, 9	lspss 17425	. . . . . . . . . . . . . . . . . 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 3507	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` ( s \ { w } ) ) )
118		vex 3116	. . . . . . . . . . . . . . . 16 |- w e. _V
119		id 22	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> x = w )
120		sneq 4037	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = w -> { x } = { w } )
121	120	difeq2d 3622	. . . . . . . . . . . . . . . . . . . 20 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( ( s u. { w } ) \ { w } ) )
122		difun2 3906	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s u. { w } ) \ { w } ) = ( s \ { w } )
123	121, 122	syl6eq 2524	. . . . . . . . . . . . . . . . . . 19 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( s \ { w } ) )
124	123	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( s \ { w } ) ) )
125	119, 124	eleq12d 2549	. . . . . . . . . . . . . . . . 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 4066	. . . . . . . . . . . . . . 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 3686	. . . . . . . . . . . . . 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 3526	. . . . . . . . . . . . . 14 |- ( z = ( s u. { w } ) -> ( C C_ z <-> C C_ ( s u. { w } ) ) )
133		difeq1 3615	. . . . . . . . . . . . . . . . . 18 |- ( z = ( s u. { w } ) -> ( z \ { x } ) = ( ( s u. { w } ) \ { x } ) )
134	133	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( z = ( s u. { w } ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( s u. { w } ) \ { x } ) ) )
135	134	eleq2d 2537	. . . . . . . . . . . . . . . 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 3066	. . . . . . . . . . . . . 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 3263	. . . . . . . . . . . 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 760	. . . . . . . . . . 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 3592	. . . . . . . . . . . . 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 3210	. . . . . . . . . . 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 3820	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( V \ ( N ` s ) ) = (/) )
148		ssdif0 3885	. . . . . . . 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 3521	. . . . . 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 17595	. . . . . . 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 2934	. 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 1377   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   C. wpss 3477   (/)c0 3785   ~Pcpw 4010   {csn 4027   U.cuni 4245   U_ciun 4325   Or wor 4799   dom cdm 4999   ` cfv 5587   [ C.] crpss 6562   cardccrd 8315   Basecbs 14489   LModclmod 17307   LSubSpclss 17373   LSpanclspn 17412  LBasisclbs 17515   LVecclvec 17543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575  ax-cnex 9547  ax-resscn 9548  ax-1cn 9549  ax-icn 9550  ax-addcl 9551  ax-addrcl 9552  ax-mulcl 9553  ax-mulrcl 9554  ax-mulcom 9555  ax-addass 9556  ax-mulass 9557  ax-distr 9558  ax-i2m1 9559  ax-1ne0 9560  ax-1rid 9561  ax-rnegex 9562  ax-rrecex 9563  ax-cnre 9564  ax-pre-lttri 9565  ax-pre-lttrn 9566  ax-pre-ltadd 9567  ax-pre-mulgt0 9568

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-isom 5596  df-riota 6244  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-rpss 6563  df-om 6680  df-1st 6784  df-2nd 6785  df-tpos 6955  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-card 8319  df-cda 8547  df-pnf 9629  df-mnf 9630  df-xr 9631  df-ltxr 9632  df-le 9633  df-sub 9806  df-neg 9807  df-nn 10536  df-2 10593  df-3 10594  df-ndx 14492  df-slot 14493  df-base 14494  df-sets 14495  df-ress 14496  df-plusg 14567  df-mulr 14568  df-0g 14696  df-mnd 15731  df-grp 15864  df-minusg 15865  df-sbg 15866  df-cmn 16603  df-abl 16604  df-mgp 16941  df-ur 16953  df-rng 16997  df-oppr 17068  df-dvdsr 17086  df-unit 17087  df-invr 17117  df-drng 17193  df-lmod 17309  df-lss 17374  df-lsp 17413  df-lbs 17516  df-lvec 17544

This theorem is referenced by:  lbsextg  17603