Theorem lbsextlem4 18129

Description: Lemma for lbsext 18131. lbsextlem3 18128 satisfies the conditions for the application of Zorn's lemma zorn 8921 (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 3526	. . . . 5 |- { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } C_ ~P V
4	2, 3	eqsstri 3474	. . . 4 |- S C_ ~P V
5		ssnum 8454	. . . 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 18126	. . 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 2404	. . . . . 6 |- ( LSubSp ` W ) = ( LSubSp ` W )
18		simpr1 1005	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y C_ S )
19		simpr2 1006	. . . . . 6 |- ( ( ph /\ ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) ) -> y =/= (/) )
20		simpr3 1007	. . . . . 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 18128	. . . . 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 1742	. . 3 |- ( ph -> A. y ( ( y C_ S /\ y =/= (/) /\ [ C.] Or y ) -> U. y e. S ) )
25		zornn0g 8919	. . 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 1232	. 2 |- ( ph -> E. s e. S A. t e. S -. s C. t )
27		simprl 758	. . . . . . . . 9 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s e. S )
28		sseq2 3466	. . . . . . . . . . 11 |- ( z = s -> ( C C_ z <-> C C_ s ) )
29		difeq1 3556	. . . . . . . . . . . . . . 15 |- ( z = s -> ( z \ { x } ) = ( s \ { x } ) )
30	29	fveq2d 5855	. . . . . . . . . . . . . 14 |- ( z = s -> ( N ` ( z \ { x } ) ) = ( N ` ( s \ { x } ) ) )
31	30	eleq2d 2474	. . . . . . . . . . . . 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 3014	. . . . . . . . . . 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 711	. . . . . . . . . 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 3211	. . . . . . . . 9 |- ( s e. S <-> ( s e. ~P V /\ ( C C_ s /\ A. x e. s -. x e. ( N ` ( s \ { x } ) ) ) ) )
36	27, 35	sylib 198	. . . . . . . 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 3967	. . . . . 6 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> s C_ V )
39		lveclmod 18074	. . . . . . . . . 10 |- ( W e. LVec -> W e. LMod )
40	10, 39	syl 17	. . . . . . . . 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 17951	. . . . . . . 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 3608	. . . . . . . . . . . 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 3609	. . . . . . . . . . . . . 14 |- { w } C_ ( s u. { w } )
47		ssnid 4003	. . . . . . . . . . . . . 14 |- w e. { w }
48	46, 47	sselii 3441	. . . . . . . . . . . . 13 |- w e. ( s u. { w } )
49	7, 9	lspssid 17953	. . . . . . . . . . . . . . . 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 3568	. . . . . . . . . . . . . . 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 3447	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. s )
55		nelne1 2734	. . . . . . . . . . . . 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 2676	. . . . . . . . . . 11 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> s =/= ( s u. { w } ) )
58		df-pss 3432	. . . . . . . . . . 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 3567	. . . . . . . . . . . . . . . 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 4119	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> { w } C_ V )
64	60, 63	unssd 3621	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> ( s u. { w } ) C_ V )
65		fvex 5861	. . . . . . . . . . . . . . 15 |- ( Base ` W ) e. _V
66	7, 65	eqeltri 2488	. . . . . . . . . . . . . 14 |- V e. _V
67	66	elpw2 4560	. . . . . . . . . . . . 13 |- ( ( s u. { w } ) e. ~P V <-> ( s u. { w } ) C_ V )
68	64, 67	sylibr 214	. . . . . . . . . . . 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 3456	. . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . 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 3583	. . . . . . . . . . . . . . . . . . . 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 717	. . . . . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. { w } -> x = w )
83	82	necon3ai 2633	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { w } i^i { x } ) = (/) <-> -. x e. { w } )
86	84, 85	sylibr 214	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3816	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( { w } i^i { x } ) = (/) <-> { w } = ( { w } \ { x } ) )
88	86, 87	sylib 198	. . . . . . . . . . . . . . . . . . . . . . . . 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 3599	. . . . . . . . . . . . . . . . . . . . . . . 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 3705	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s u. { w } ) \ { x } ) = ( ( s \ { x } ) u. ( { w } \ { x } ) )
91	89, 90	syl6reqr 2464	. . . . . . . . . . . . . . . . . . . . . . 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 5855	. . . . . . . . . . . . . . . . . . . . . 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 2494	. . . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. x e. s -. x e. ( N ` ( s \ { x } ) ) -> ( x e. s -> -. x e. ( N ` ( s \ { x } ) ) ) )
97	95, 78, 96	sylc 61	. . . . . . . . . . . . . . . . . . . . 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 3427	. . . . . . . . . . . . . . . . . . . 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 18111	. . . . . . . . . . . . . . . . . . . 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 1234	. . . . . . . . . . . . . . . . . . 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 3849	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s \ { x } ) u. { x } ) = ( s u. { x } )
102	78	snssd 4119	. . . . . . . . . . . . . . . . . . . . . 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 3618	. . . . . . . . . . . . . . . . . . . . . 22 |- ( { x } C_ s <-> ( s u. { x } ) = s )
104	102, 103	sylib 198	. . . . . . . . . . . . . . . . . . . . 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 2457	. . . . . . . . . . . . . . . . . . . 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 5855	. . . . . . . . . . . . . . . . . . 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 2494	. . . . . . . . . . . . . . . . . 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 179	. . . . . . . . . . . . . . . 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 214	. . . . . . . . . . . . . . 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 2818	. . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( s \ { w } ) C_ s )
114	7, 9	lspss 17952	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. LMod /\ s C_ V /\ ( s \ { w } ) C_ s ) -> ( N ` ( s \ { w } ) ) C_ ( N ` s ) )
115	41, 38, 113, 114	syl3anc 1232	. . . . . . . . . . . . . . . . 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 3447	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) /\ w e. ( V \ ( N ` s ) ) ) -> -. w e. ( N ` ( s \ { w } ) ) )
118		vex 3064	. . . . . . . . . . . . . . . 16 |- w e. _V
119		id 23	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> x = w )
120		sneq 3984	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = w -> { x } = { w } )
121	120	difeq2d 3563	. . . . . . . . . . . . . . . . . . . 20 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( ( s u. { w } ) \ { w } ) )
122		difun2 3853	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s u. { w } ) \ { w } ) = ( s \ { w } )
123	121, 122	syl6eq 2461	. . . . . . . . . . . . . . . . . . 19 |- ( x = w -> ( ( s u. { w } ) \ { x } ) = ( s \ { w } ) )
124	123	fveq2d 5855	. . . . . . . . . . . . . . . . . 18 |- ( x = w -> ( N ` ( ( s u. { w } ) \ { x } ) ) = ( N ` ( s \ { w } ) ) )
125	119, 124	eleq12d 2486	. . . . . . . . . . . . . . . . 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 4013	. . . . . . . . . . . . . . 15 |- ( A. x e. { w } -. x e. ( N ` ( ( s u. { w } ) \ { x } ) ) <-> -. w e. ( N ` ( s \ { w } ) ) )
128	117, 127	sylibr 214	. . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . 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 3466	. . . . . . . . . . . . . 14 |- ( z = ( s u. { w } ) -> ( C C_ z <-> C C_ ( s u. { w } ) ) )
133		difeq1 3556	. . . . . . . . . . . . . . . . . 18 |- ( z = ( s u. { w } ) -> ( z \ { x } ) = ( ( s u. { w } ) \ { x } ) )
134	133	fveq2d 5855	. . . . . . . . . . . . . . . . 17 |- ( z = ( s u. { w } ) -> ( N ` ( z \ { x } ) ) = ( N ` ( ( s u. { w } ) \ { x } ) ) )
135	134	eleq2d 2474	. . . . . . . . . . . . . . . 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 3014	. . . . . . . . . . . . . 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 711	. . . . . . . . . . . . 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 3211	. . . . . . . . . . . 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 765	. . . . . . . . . . 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 3533	. . . . . . . . . . . . 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 3158	. . . . . . . . . . 11 |- ( ( s u. { w } ) e. S -> ( A. t e. S -. s C. t -> -. s C. ( s u. { w } ) ) )
145	140, 141, 144	sylc 61	. . . . . . . . . 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 3776	. . . . . . . 8 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> ( V \ ( N ` s ) ) = (/) )
148		ssdif0 3830	. . . . . . . 8 |- ( V C_ ( N ` s ) <-> ( V \ ( N ` s ) ) = (/) )
149	147, 148	sylibr 214	. . . . . . 7 |- ( ( ph /\ ( s e. S /\ A. t e. S -. s C. t ) ) -> V C_ ( N ` s ) )
150	43, 149	eqssd 3461	. . . . . 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 18122	. . . . . . 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 1182	. . . . 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 2877	. 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 186   /\ wa 369   /\ w3a 976   A.wal 1405   = wceq 1407   e. wcel 1844   =/= wne 2600   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3061   \ cdif 3413   u. cun 3414   i^i cin 3415   C_ wss 3416   C. wpss 3417   (/)c0 3740   ~Pcpw 3957   {csn 3974   U.cuni 4193   U_ciun 4273   Or wor 4745   dom cdm 4825   ` cfv 5571   [ C.] crpss 6563   cardccrd 8350   Basecbs 14843   LModclmod 17834   LSubSpclss 17900   LSpanclspn 17939  LBasisclbs 18042   LVecclvec 18070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-se 4785  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-isom 5580  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-rpss 6564  df-om 6686  df-1st 6786  df-2nd 6787  df-tpos 6960  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-card 8354  df-cda 8582  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-nn 10579  df-2 10637  df-3 10638  df-ndx 14846  df-slot 14847  df-base 14848  df-sets 14849  df-ress 14850  df-plusg 14924  df-mulr 14925  df-0g 15058  df-mgm 16198  df-sgrp 16237  df-mnd 16247  df-grp 16383  df-minusg 16384  df-sbg 16385  df-cmn 17126  df-abl 17127  df-mgp 17464  df-ur 17476  df-ring 17522  df-oppr 17594  df-dvdsr 17612  df-unit 17613  df-invr 17643  df-drng 17720  df-lmod 17836  df-lss 17901  df-lsp 17940  df-lbs 18043  df-lvec 18071

This theorem is referenced by:  lbsextg  18130