Theorem islindf4 27176

Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015.)

Hypotheses

Ref	Expression
islindf4.b	|- B = ( Base ` W )
islindf4.r	|- R = (Scalar ` W )
islindf4.t	|- .x. = ( .s ` W )
islindf4.z	|- .0. = ( 0g ` W )
islindf4.y	|- Y = ( 0g ` R )
islindf4.l	|- L = ( Base ` ( R freeLMod I ) )

Assertion

Ref	Expression
islindf4	|- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> x = ( I X. { Y } ) ) ) )

Distinct variable groups:   x, B   x, F   x, I   x, L   x, R   x, .x.   x, W   x, X   x, Y   x, .0.

Proof of Theorem islindf4

Dummy variables j k l y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raldifsni 26624	. . . . 5 |- ( A. l e. ( ( Base ` R ) \ { Y } ) -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. l e. ( Base ` R ) ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) -> l = Y ) )
2		simpll1 996	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> W e. LMod )
3		simprll 739	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> l e. ( Base ` R ) )
4		ffvelrn 5827	. . . . . . . . . . . . . . . . . 18 |- ( ( F : I --> B /\ j e. I ) -> ( F ` j ) e. B )
5	4	3ad2antl3 1121	. . . . . . . . . . . . . . . . 17 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F ` j ) e. B )
6	5	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( F ` j ) e. B )
7		islindf4.b	. . . . . . . . . . . . . . . . 17 |- B = ( Base ` W )
8		islindf4.r	. . . . . . . . . . . . . . . . 17 |- R = (Scalar ` W )
9		islindf4.t	. . . . . . . . . . . . . . . . 17 |- .x. = ( .s ` W )
10		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( inv g ` W ) = ( inv g ` W )
11		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( inv g ` R ) = ( inv g ` R )
12		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
13	7, 8, 9, 10, 11, 12	lmodvsinv 16067	. . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ l e. ( Base ` R ) /\ ( F ` j ) e. B ) -> ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( ( inv g ` W ) ` ( l .x. ( F ` j ) ) ) )
14	2, 3, 6, 13	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( ( inv g ` W ) ` ( l .x. ( F ` j ) ) ) )
15	14	eqeq1d 2412	. . . . . . . . . . . . . 14 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) <-> ( ( inv g ` W ) ` ( l .x. ( F ` j ) ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) )
16		lmodgrp 15912	. . . . . . . . . . . . . . . 16 |- ( W e. LMod -> W e. Grp )
17	2, 16	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> W e. Grp )
18	7, 8, 9, 12	lmodvscl 15922	. . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ l e. ( Base ` R ) /\ ( F ` j ) e. B ) -> ( l .x. ( F ` j ) ) e. B )
19	2, 3, 6, 18	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( l .x. ( F ` j ) ) e. B )
20		islindf4.z	. . . . . . . . . . . . . . . 16 |- .0. = ( 0g ` W )
21		lmodcmn 15947	. . . . . . . . . . . . . . . . 17 |- ( W e. LMod -> W e. CMnd )
22	2, 21	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> W e. CMnd )
23		simpll2 997	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> I e. X )
24		difexg 4311	. . . . . . . . . . . . . . . . 17 |- ( I e. X -> ( I \ { j } ) e. _V )
25	23, 24	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( I \ { j } ) e. _V )
26		simprlr 740	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> y e. ( ( Base ` R ) ^m ( I \ { j } ) ) )
27		elmapi 6997	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> y : ( I \ { j } ) --> ( Base ` R ) )
28	26, 27	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> y : ( I \ { j } ) --> ( Base ` R ) )
29		simpll3 998	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> F : I --> B )
30		difss 3434	. . . . . . . . . . . . . . . . . 18 |- ( I \ { j } ) C_ I
31		fssres 5569	. . . . . . . . . . . . . . . . . 18 |- ( ( F : I --> B /\ ( I \ { j } ) C_ I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
32	29, 30, 31	sylancl 644	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
33	8, 12, 9, 7, 2, 28, 32, 25	lcomf 26636	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( y o F .x. ( F |` ( I \ { j } ) ) ) : ( I \ { j } ) --> B )
34		islindf4.y	. . . . . . . . . . . . . . . . 17 |- Y = ( 0g ` R )
35		simprr 734	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( `' y " ( _V \ { Y } ) ) e. Fin )
36	8, 12, 9, 7, 2, 28, 32, 25, 20, 34, 35	lcomfsup 26637	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( `' ( y o F .x. ( F |` ( I \ { j } ) ) ) " ( _V \ { .0. } ) ) e. Fin )
37	7, 20, 22, 25, 33, 36	gsumcl 15476	. . . . . . . . . . . . . . 15 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) e. B )
38		eqid 2404	. . . . . . . . . . . . . . . 16 |- ( +g ` W ) = ( +g ` W )
39	7, 38, 20, 10	grpinvid2 14809	. . . . . . . . . . . . . . 15 |- ( ( W e. Grp /\ ( l .x. ( F ` j ) ) e. B /\ ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) e. B ) -> ( ( ( inv g ` W ) ` ( l .x. ( F ` j ) ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) <-> ( ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = .0. ) )
40	17, 19, 37, 39	syl3anc 1184	. . . . . . . . . . . . . 14 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( inv g ` W ) ` ( l .x. ( F ` j ) ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) <-> ( ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = .0. ) )
41		simplr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> j e. I )
42		fsnunf2 5891	. . . . . . . . . . . . . . . . . . 19 |- ( ( y : ( I \ { j } ) --> ( Base ` R ) /\ j e. I /\ l e. ( Base ` R ) ) -> ( y u. { <. j , l >. } ) : I --> ( Base ` R ) )
43	28, 41, 3, 42	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( y u. { <. j , l >. } ) : I --> ( Base ` R ) )
44	8, 12, 9, 7, 2, 43, 29, 23	lcomf 26636	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( y u. { <. j , l >. } ) o F .x. F ) : I --> B )
45		funsnfsup 26633	. . . . . . . . . . . . . . . . . . . 20 |- ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin <-> ( `' y " ( _V \ { Y } ) ) e. Fin )
46	45	biimpri 198	. . . . . . . . . . . . . . . . . . 19 |- ( ( `' y " ( _V \ { Y } ) ) e. Fin -> ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin )
47	46	ad2antll 710	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin )
48	8, 12, 9, 7, 2, 43, 29, 23, 20, 34, 47	lcomfsup 26637	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( `' ( ( y u. { <. j , l >. } ) o F .x. F ) " ( _V \ { .0. } ) ) e. Fin )
49		incom 3493	. . . . . . . . . . . . . . . . . . 19 |- ( ( I \ { j } ) i^i { j } ) = ( { j } i^i ( I \ { j } ) )
50		disjdif 3660	. . . . . . . . . . . . . . . . . . 19 |- ( { j } i^i ( I \ { j } ) ) = (/)
51	49, 50	eqtri 2424	. . . . . . . . . . . . . . . . . 18 |- ( ( I \ { j } ) i^i { j } ) = (/)
52	51	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( I \ { j } ) i^i { j } ) = (/) )
53		difsnid 3904	. . . . . . . . . . . . . . . . . . 19 |- ( j e. I -> ( ( I \ { j } ) u. { j } ) = I )
54	53	eqcomd 2409	. . . . . . . . . . . . . . . . . 18 |- ( j e. I -> I = ( ( I \ { j } ) u. { j } ) )
55	41, 54	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> I = ( ( I \ { j } ) u. { j } ) )
56	7, 20, 38, 22, 23, 44, 48, 52, 55	gsumsplit 15485	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = ( ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` ( I \ { j } ) ) ) ( +g ` W ) ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) ) ) )
57		vex 2919	. . . . . . . . . . . . . . . . . . . . 21 |- y e. _V
58		snex 4365	. . . . . . . . . . . . . . . . . . . . 21 |- { <. j , l >. } e. _V
59	57, 58	unex 4666	. . . . . . . . . . . . . . . . . . . 20 |- ( y u. { <. j , l >. } ) e. _V
60		simpl3 962	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F : I --> B )
61		simpl2 961	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> I e. X )
62		fex 5928	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F : I --> B /\ I e. X ) -> F e. _V )
63	60, 61, 62	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F e. _V )
64	63	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> F e. _V )
65		offres 6278	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y u. { <. j , l >. } ) e. _V /\ F e. _V ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` ( I \ { j } ) ) = ( ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) o F .x. ( F |` ( I \ { j } ) ) ) )
66	59, 64, 65	sylancr 645	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` ( I \ { j } ) ) = ( ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) o F .x. ( F |` ( I \ { j } ) ) ) )
67		ffn 5550	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y : ( I \ { j } ) --> ( Base ` R ) -> y Fn ( I \ { j } ) )
68	28, 67	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> y Fn ( I \ { j } ) )
69		neldifsn 3889	. . . . . . . . . . . . . . . . . . . . 21 |- -. j e. ( I \ { j } )
70		fsnunres 5893	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y Fn ( I \ { j } ) /\ -. j e. ( I \ { j } ) ) -> ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) = y )
71	68, 69, 70	sylancl 644	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) = y )
72	71	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) o F .x. ( F |` ( I \ { j } ) ) ) = ( y o F .x. ( F |` ( I \ { j } ) ) ) )
73	66, 72	eqtrd 2436	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` ( I \ { j } ) ) = ( y o F .x. ( F |` ( I \ { j } ) ) ) )
74	73	oveq2d 6056	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` ( I \ { j } ) ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) )
75		ffn 5550	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y u. { <. j , l >. } ) o F .x. F ) : I --> B -> ( ( y u. { <. j , l >. } ) o F .x. F ) Fn I )
76	44, 75	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( y u. { <. j , l >. } ) o F .x. F ) Fn I )
77		fnressn 5877	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y u. { <. j , l >. } ) o F .x. F ) Fn I /\ j e. I ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) = { <. j , ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) >. } )
78	76, 41, 77	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) = { <. j , ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) >. } )
79		ffn 5550	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y u. { <. j , l >. } ) : I --> ( Base ` R ) -> ( y u. { <. j , l >. } ) Fn I )
80	43, 79	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( y u. { <. j , l >. } ) Fn I )
81		ffn 5550	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( F : I --> B -> F Fn I )
82	29, 81	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> F Fn I )
83		fnfvof 6276	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( y u. { <. j , l >. } ) Fn I /\ F Fn I ) /\ ( I e. X /\ j e. I ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) = ( ( ( y u. { <. j , l >. } ) ` j ) .x. ( F ` j ) ) )
84	80, 82, 23, 41, 83	syl22anc 1185	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) = ( ( ( y u. { <. j , l >. } ) ` j ) .x. ( F ` j ) ) )
85		fndm 5503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y Fn ( I \ { j } ) -> dom y = ( I \ { j } ) )
86	85	eleq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y Fn ( I \ { j } ) -> ( j e. dom y <-> j e. ( I \ { j } ) ) )
87	69, 86	mtbiri 295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y Fn ( I \ { j } ) -> -. j e. dom y )
88		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- j e. _V
89		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- l e. _V
90		fsnunfv 5892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( j e. _V /\ l e. _V /\ -. j e. dom y ) -> ( ( y u. { <. j , l >. } ) ` j ) = l )
91	88, 89, 90	mp3an12 1269	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. j e. dom y -> ( ( y u. { <. j , l >. } ) ` j ) = l )
92	68, 87, 91	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( y u. { <. j , l >. } ) ` j ) = l )
93	92	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) ` j ) .x. ( F ` j ) ) = ( l .x. ( F ` j ) ) )
94	84, 93	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) = ( l .x. ( F ` j ) ) )
95	94	opeq2d 3951	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> <. j , ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) >. = <. j , ( l .x. ( F ` j ) ) >. )
96	95	sneqd 3787	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> { <. j , ( ( ( y u. { <. j , l >. } ) o F .x. F ) ` j ) >. } = { <. j , ( l .x. ( F ` j ) ) >. } )
97		ovex 6065	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l .x. ( F ` j ) ) e. _V
98		fmptsn 5881	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( j e. _V /\ ( l .x. ( F ` j ) ) e. _V ) -> { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) ) )
99	88, 97, 98	mp2an 654	. . . . . . . . . . . . . . . . . . . . 21 |- { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) )
100	99	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) ) )
101	78, 96, 100	3eqtrd 2440	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) = ( x e. { j } |-> ( l .x. ( F ` j ) ) ) )
102	101	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) ) = ( W gsumg ( x e. { j } |-> ( l .x. ( F ` j ) ) ) ) )
103		cmnmnd 15382	. . . . . . . . . . . . . . . . . . . 20 |- ( W e. CMnd -> W e. Mnd )
104	22, 103	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> W e. Mnd )
105	88	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> j e. _V )
106		eqidd 2405	. . . . . . . . . . . . . . . . . . . 20 |- ( x = j -> ( l .x. ( F ` j ) ) = ( l .x. ( F ` j ) ) )
107	7, 106	gsumsn 15498	. . . . . . . . . . . . . . . . . . 19 |- ( ( W e. Mnd /\ j e. _V /\ ( l .x. ( F ` j ) ) e. B ) -> ( W gsumg ( x e. { j } |-> ( l .x. ( F ` j ) ) ) ) = ( l .x. ( F ` j ) ) )
108	104, 105, 19, 107	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( W gsumg ( x e. { j } |-> ( l .x. ( F ` j ) ) ) ) = ( l .x. ( F ` j ) ) )
109	102, 108	eqtrd 2436	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) ) = ( l .x. ( F ` j ) ) )
110	74, 109	oveq12d 6058	. . . . . . . . . . . . . . . 16 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` ( I \ { j } ) ) ) ( +g ` W ) ( W gsumg ( ( ( y u. { <. j , l >. } ) o F .x. F ) |` { j } ) ) ) = ( ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) )
111	56, 110	eqtr2d 2437	. . . . . . . . . . . . . . 15 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) )
112	111	eqeq1d 2412	. . . . . . . . . . . . . 14 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = .0. <-> ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. ) )
113	15, 40, 112	3bitrd 271	. . . . . . . . . . . . 13 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) <-> ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. ) )
114	92	eqcomd 2409	. . . . . . . . . . . . . 14 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> l = ( ( y u. { <. j , l >. } ) ` j ) )
115	114	eqeq1d 2412	. . . . . . . . . . . . 13 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( l = Y <-> ( ( y u. { <. j , l >. } ) ` j ) = Y ) )
116	113, 115	imbi12d 312	. . . . . . . . . . . 12 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) ) -> ( ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) <-> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
117	116	anassrs 630	. . . . . . . . . . 11 |- ( ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) ) /\ ( `' y " ( _V \ { Y } ) ) e. Fin ) -> ( ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) <-> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
118	117	pm5.74da 669	. . . . . . . . . 10 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) ) -> ( ( ( `' y " ( _V \ { Y } ) ) e. Fin -> ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) ) <-> ( ( `' y " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
119		impexp 434	. . . . . . . . . 10 |- ( ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> ( ( `' y " ( _V \ { Y } ) ) e. Fin -> ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) ) )
120	45	imbi1i 316	. . . . . . . . . 10 |- ( ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) <-> ( ( `' y " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
121	118, 119, 120	3bitr4g 280	. . . . . . . . 9 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) ) -> ( ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
122	121	2ralbidva 2706	. . . . . . . 8 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
123		cnveq 5005	. . . . . . . . . . . . 13 |- ( x = ( y u. { <. j , l >. } ) -> `' x = `' ( y u. { <. j , l >. } ) )
124	123	imaeq1d 5161	. . . . . . . . . . . 12 |- ( x = ( y u. { <. j , l >. } ) -> ( `' x " ( _V \ { Y } ) ) = ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) )
125	124	eleq1d 2470	. . . . . . . . . . 11 |- ( x = ( y u. { <. j , l >. } ) -> ( ( `' x " ( _V \ { Y } ) ) e. Fin <-> ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin ) )
126		oveq1 6047	. . . . . . . . . . . . . 14 |- ( x = ( y u. { <. j , l >. } ) -> ( x o F .x. F ) = ( ( y u. { <. j , l >. } ) o F .x. F ) )
127	126	oveq2d 6056	. . . . . . . . . . . . 13 |- ( x = ( y u. { <. j , l >. } ) -> ( W gsumg ( x o F .x. F ) ) = ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) )
128	127	eqeq1d 2412	. . . . . . . . . . . 12 |- ( x = ( y u. { <. j , l >. } ) -> ( ( W gsumg ( x o F .x. F ) ) = .0. <-> ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. ) )
129		fveq1 5686	. . . . . . . . . . . . 13 |- ( x = ( y u. { <. j , l >. } ) -> ( x ` j ) = ( ( y u. { <. j , l >. } ) ` j ) )
130	129	eqeq1d 2412	. . . . . . . . . . . 12 |- ( x = ( y u. { <. j , l >. } ) -> ( ( x ` j ) = Y <-> ( ( y u. { <. j , l >. } ) ` j ) = Y ) )
131	128, 130	imbi12d 312	. . . . . . . . . . 11 |- ( x = ( y u. { <. j , l >. } ) -> ( ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) <-> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
132	125, 131	imbi12d 312	. . . . . . . . . 10 |- ( x = ( y u. { <. j , l >. } ) -> ( ( ( `' x " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) <-> ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
133	132	ralxpmap 26632	. . . . . . . . 9 |- ( j e. I -> ( A. x e. ( ( Base ` R ) ^m I ) ( ( `' x " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) <-> A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
134	133	adantl 453	. . . . . . . 8 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. x e. ( ( Base ` R ) ^m I ) ( ( `' x " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) <-> A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' ( y u. { <. j , l >. } ) " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( ( y u. { <. j , l >. } ) o F .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
135	122, 134	bitr4d 248	. . . . . . 7 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> A. x e. ( ( Base ` R ) ^m I ) ( ( `' x " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) ) )
136		cnveq 5005	. . . . . . . . . 10 |- ( z = x -> `' z = `' x )
137	136	imaeq1d 5161	. . . . . . . . 9 |- ( z = x -> ( `' z " ( _V \ { Y } ) ) = ( `' x " ( _V \ { Y } ) ) )
138	137	eleq1d 2470	. . . . . . . 8 |- ( z = x -> ( ( `' z " ( _V \ { Y } ) ) e. Fin <-> ( `' x " ( _V \ { Y } ) ) e. Fin ) )
139	138	ralrab 3056	. . . . . . 7 |- ( A. x e. { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) <-> A. x e. ( ( Base ` R ) ^m I ) ( ( `' x " ( _V \ { Y } ) ) e. Fin -> ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
140	135, 139	syl6bbr 255	. . . . . 6 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> A. x e. { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
141		resima 5137	. . . . . . . . . . . . 13 |- ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) = ( F " ( I \ { j } ) )
142	141	eqcomi 2408	. . . . . . . . . . . 12 |- ( F " ( I \ { j } ) ) = ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) )
143	142	fveq2i 5690	. . . . . . . . . . 11 |- ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) = ( ( LSpan ` W ) ` ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) )
144	143	eleq2i 2468	. . . . . . . . . 10 |- ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) ) )
145		eqid 2404	. . . . . . . . . . 11 |- ( LSpan ` W ) = ( LSpan ` W )
146	60, 30, 31	sylancl 644	. . . . . . . . . . 11 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
147		simpl1 960	. . . . . . . . . . 11 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> W e. LMod )
148	24	3ad2ant2 979	. . . . . . . . . . . 12 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( I \ { j } ) e. _V )
149	148	adantr 452	. . . . . . . . . . 11 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( I \ { j } ) e. _V )
150	145, 7, 12, 8, 34, 9, 146, 147, 149	ellspd 27122	. . . . . . . . . 10 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) ) <-> E. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) ) )
151	144, 150	syl5bb 249	. . . . . . . . 9 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> E. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) ) )
152	151	imbi1d 309	. . . . . . . 8 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) -> l = Y ) <-> ( E. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) ) )
153		r19.23v 2782	. . . . . . . 8 |- ( A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> ( E. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) )
154	152, 153	syl6bbr 255	. . . . . . 7 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) -> l = Y ) <-> A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) ) )
155	154	ralbidv 2686	. . . . . 6 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. l e. ( Base ` R ) ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) -> l = Y ) <-> A. l e. ( Base ` R ) A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( ( `' y " ( _V \ { Y } ) ) e. Fin /\ ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) = ( W gsumg ( y o F .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) ) )
156		fvex 5701	. . . . . . . . . . . 12 |- (Scalar ` W ) e. _V
157	8, 156	eqeltri 2474	. . . . . . . . . . 11 |- R e. _V
158		eqid 2404	. . . . . . . . . . . 12 |- ( R freeLMod I ) = ( R freeLMod I )
159		eqid 2404	. . . . . . . . . . . 12 |- { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } = { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin }
160	158, 12, 34, 159	frlmbas 27091	. . . . . . . . . . 11 |- ( ( R e. _V /\ I e. X ) -> { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } = ( Base ` ( R freeLMod I ) ) )
161	157, 160	mpan 652	. . . . . . . . . 10 |- ( I e. X -> { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } = ( Base ` ( R freeLMod I ) ) )
162	161	3ad2ant2 979	. . . . . . . . 9 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } = ( Base ` ( R freeLMod I ) ) )
163	162	adantr 452	. . . . . . . 8 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } = ( Base ` ( R freeLMod I ) ) )
164		islindf4.l	. . . . . . . 8 |- L = ( Base ` ( R freeLMod I ) )
165	163, 164	syl6reqr 2455	. . . . . . 7 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> L = { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } )
166	165	raleqdv 2870	. . . . . 6 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) <-> A. x e. { z e. ( ( Base ` R ) ^m I ) | ( `' z " ( _V \ { Y } ) ) e. Fin } ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
167	140, 155, 166	3bitr4d 277	. . . . 5 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. l e. ( Base ` R ) ( ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) -> l = Y ) <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
168	1, 167	syl5bb 249	. . . 4 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. l e. ( ( Base ` R ) \ { Y } ) -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
169	8	lmodfgrp 15914	. . . . . . . 8 |- ( W e. LMod -> R e. Grp )
170	12, 34, 11	grpinvnzcl 14818	. . . . . . . 8 |- ( ( R e. Grp /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( inv g ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
171	169, 170	sylan 458	. . . . . . 7 |- ( ( W e. LMod /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( inv g ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
172	12, 34, 11	grpinvnzcl 14818	. . . . . . . . 9 |- ( ( R e. Grp /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( inv g ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
173	169, 172	sylan 458	. . . . . . . 8 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( inv g ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
174		eldifi 3429	. . . . . . . . . 10 |- ( k e. ( ( Base ` R ) \ { Y } ) -> k e. ( Base ` R ) )
175	12, 11	grpinvinv 14813	. . . . . . . . . 10 |- ( ( R e. Grp /\ k e. ( Base ` R ) ) -> ( ( inv g ` R ) ` ( ( inv g ` R ) ` k ) ) = k )
176	169, 174, 175	syl2an 464	. . . . . . . . 9 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( inv g ` R ) ` ( ( inv g ` R ) ` k ) ) = k )
177	176	eqcomd 2409	. . . . . . . 8 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> k = ( ( inv g ` R ) ` ( ( inv g ` R ) ` k ) ) )
178		fveq2 5687	. . . . . . . . . 10 |- ( l = ( ( inv g ` R ) ` k ) -> ( ( inv g ` R ) ` l ) = ( ( inv g ` R ) ` ( ( inv g ` R ) ` k ) ) )
179	178	eqeq2d 2415	. . . . . . . . 9 |- ( l = ( ( inv g ` R ) ` k ) -> ( k = ( ( inv g ` R ) ` l ) <-> k = ( ( inv g ` R ) ` ( ( inv g ` R ) ` k ) ) ) )
180	179	rspcev 3012	. . . . . . . 8 |- ( ( ( ( inv g ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) /\ k = ( ( inv g ` R ) ` ( ( inv g ` R ) ` k ) ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( inv g ` R ) ` l ) )
181	173, 177, 180	syl2anc 643	. . . . . . 7 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( inv g ` R ) ` l ) )
182		oveq1 6047	. . . . . . . . . 10 |- ( k = ( ( inv g ` R ) ` l ) -> ( k .x. ( F ` j ) ) = ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) )
183	182	eleq1d 2470	. . . . . . . . 9 |- ( k = ( ( inv g ` R ) ` l ) -> ( ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
184	183	notbid 286	. . . . . . . 8 |- ( k = ( ( inv g ` R ) ` l ) -> ( -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
185	184	adantl 453	. . . . . . 7 |- ( ( W e. LMod /\ k = ( ( inv g ` R ) ` l ) ) -> ( -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
186	171, 181, 185	ralxfrd 4696	. . . . . 6 |- ( W e. LMod -> ( A. k e. ( ( Base ` R ) \ { Y } ) -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. l e. ( ( Base ` R ) \ { Y } ) -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
187	186	3ad2ant1 978	. . . . 5 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( A. k e. ( ( Base ` R ) \ { Y } ) -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. l e. ( ( Base ` R ) \ { Y } ) -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
188	187	adantr 452	. . . 4 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. k e. ( ( Base ` R ) \ { Y } ) -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. l e. ( ( Base ` R ) \ { Y } ) -. ( ( ( inv g ` R ) ` l ) .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
189		simplr 732	. . . . . . . 8 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> j e. I )
190		fvex 5701	. . . . . . . . . 10 |- ( 0g ` R ) e. _V
191	34, 190	eqeltri 2474	. . . . . . . . 9 |- Y e. _V
192	191	fvconst2 5906	. . . . . . . 8 |- ( j e. I -> ( ( I X. { Y } ) ` j ) = Y )
193	189, 192	syl 16	. . . . . . 7 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( I X. { Y } ) ` j ) = Y )
194	193	eqeq2d 2415	. . . . . 6 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( x ` j ) = ( ( I X. { Y } ) ` j ) <-> ( x ` j ) = Y ) )
195	194	imbi2d 308	. . . . 5 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
196	195	ralbidva 2682	. . . 4 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
197	168, 188, 196	3bitr4d 277	. . 3 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. k e. ( ( Base ` R ) \ { Y } ) -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
198	197	ralbidva 2682	. 2 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( A. j e. I A. k e. ( ( Base ` R ) \ { Y } ) -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) <-> A. j e. I A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
199	7, 9, 145, 8, 12, 34	islindf2 27152	. 2 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. j e. I A. k e. ( ( Base ` R ) \ { Y } ) -. ( k .x. ( F ` j ) ) e. ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) ) )
200	158, 12, 164	frlmbasf 27096	. . . . . . . 8 |- ( ( I e. X /\ x e. L ) -> x : I --> ( Base ` R ) )
201	200	3ad2antl2 1120	. . . . . . 7 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x : I --> ( Base ` R ) )
202		ffn 5550	. . . . . . 7 |- ( x : I --> ( Base ` R ) -> x Fn I )
203	201, 202	syl 16	. . . . . 6 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x Fn I )
204		fnconstg 5590	. . . . . . 7 |- ( Y e. _V -> ( I X. { Y } ) Fn I )
205	191, 204	ax-mp 8	. . . . . 6 |- ( I X. { Y } ) Fn I
206		eqfnfv 5786	. . . . . 6 |- ( ( x Fn I /\ ( I X. { Y } ) Fn I ) -> ( x = ( I X. { Y } ) <-> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
207	203, 205, 206	sylancl 644	. . . . 5 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> ( x = ( I X. { Y } ) <-> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
208	207	imbi2d 308	. . . 4 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> ( ( ( W gsumg ( x o F .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> ( ( W gsumg ( x o F .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
209	208	ralbidva 2682	. . 3 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
210		r19.21v 2753	. . . . 5 |- ( A. j e. I ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> ( ( W gsumg ( x o F .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
211	210	ralbii 2690	. . . 4 |- ( A. x e. L A. j e. I ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
212		ralcom 2828	. . . 4 |- ( A. x e. L A. j e. I ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. j e. I A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
213	211, 212	bitr3i 243	. . 3 |- ( A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. j e. I A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
214	209, 213	syl6bb 253	. 2 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> A. j e. I A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
215	198, 199, 214	3bitr4d 277	1 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. x e. L ( ( W gsumg ( x o F .x. F ) ) = .0. -> x = ( I X. { Y } ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   (/)c0 3588   {csn 3774   <.cop 3777   class class class wbr 4172   e. cmpt 4226   X. cxp 4835   `'ccnv 4836   dom cdm 4837   |` cres 4839   "cima 4840   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   o Fcof 6262   ^m cmap 6977   Fincfn 7068   Basecbs 13424   +g cplusg 13484  Scalarcsca 13487   .scvsca 13488   0gc0g 13678   gsum_g cgsu 13679   Mndcmnd 14639   Grpcgrp 14640   inv gcminusg 14641  CMndccmn 15367   LModclmod 15905   LSpanclspn 16002   freeLMod cfrlm 27080   LIndF clindf 27142

This theorem is referenced by:  islindf5  27177

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-inf2 7552  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-iin 4056  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-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  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-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-hom 13508  df-cco 13509  df-prds 13626  df-pws 13628  df-0g 13682  df-gsum 13683  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-mhm 14693  df-submnd 14694  df-grp 14767  df-minusg 14768  df-sbg 14769  df-mulg 14770  df-subg 14896  df-ghm 14959  df-cntz 15071  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-ur 15620  df-subrg 15821  df-lmod 15907  df-lss 15964  df-lsp 16003  df-lmhm 16053  df-lbs 16102  df-sra 16199  df-rgmod 16200  df-nzr 16284  df-dsmm 27066  df-frlm 27082  df-uvc 27083  df-lindf 27144