Theorem islindeps2

Description: Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islindeps2.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	islindeps2.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
	islindeps2.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	islindeps2.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	islindeps2.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	islindeps2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → 𝑆 linDepS 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		islindeps2.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		islindeps2.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
3		islindeps2.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
4		islindeps2.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
5		islindeps2.0	⊢ 0 = ( 0g ‘ 𝑅 )
6		id	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) )
7	6	3adant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) )
8	7	ad3antrrr	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) )
9		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11	4 10	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐸 )
12	9 11	syl	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ∈ 𝐸 )
13	12	3ad2ant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( 1r ‘ 𝑅 ) ∈ 𝐸 )
14	13	ad3antrrr	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐸 )
15		simpllr	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → 𝑠 ∈ 𝑆 )
16		simplr	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) )
17	14 15 16	3jca	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( ( 1r ‘ 𝑅 ) ∈ 𝐸 ∧ 𝑠 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) )
18		simprl	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → 𝑓 finSupp 0 )
19		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
20		eqid	⊢ ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) )
21	1 3 4 5 2 19 20	lincext2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ( 1r ‘ 𝑅 ) ∈ 𝐸 ∧ 𝑠 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ 𝑓 finSupp 0 ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 )
22	8 17 18 21	syl3anc	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 )
23		simpl1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → 𝑀 ∈ LMod )
24		elelpwi	⊢ ( ( 𝑠 ∈ 𝑆 ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝐵 )
25	24	expcom	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑠 ∈ 𝑆 → 𝑠 ∈ 𝐵 ) )
26	25	3ad2ant2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( 𝑠 ∈ 𝑆 → 𝑠 ∈ 𝐵 ) )
27	26	imp	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝐵 )
28		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
29	1 3 28 10	lmodvs1	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = 𝑠 )
30	23 27 29	syl2anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = 𝑠 )
31	30	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = 𝑠 )
32		id	⊢ ( ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 → ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 )
33	32	eqcomd	⊢ ( ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 → 𝑠 = ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) )
34	33	adantl	⊢ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → 𝑠 = ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) )
35	31 34	sylan9eq	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) )
36	1 3 4 5 2 19 20	lincext3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ( 1r ‘ 𝑅 ) ∈ 𝐸 ∧ 𝑠 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑀 ) 𝑠 ) = ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )
37	8 17 18 35 36	syl112anc	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )
38	22 37	jca	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
39		eqidd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) )
40		iftrue	⊢ ( 𝑧 = 𝑠 → if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
41	40	adantl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑧 = 𝑠 ) → if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
42		simpr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑆 )
43		fvexd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ V )
44	39 41 42 43	fvmptd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
45		nzrneg1ne0	⊢ ( 𝑅 ∈ NzRing → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ ( 0g ‘ 𝑅 ) )
46	5	a1i	⊢ ( 𝑅 ∈ NzRing → 0 = ( 0g ‘ 𝑅 ) )
47	45 46	neeqtrrd	⊢ ( 𝑅 ∈ NzRing → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ 0 )
48	47	3ad2ant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ 0 )
49	48	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ≠ 0 )
50	44 49	eqnetrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 )
51	50	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 )
52	51	adantr	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 )
53	1 3 4 5 2 19 20	lincext1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ( 1r ‘ 𝑅 ) ∈ 𝐸 ∧ 𝑠 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m 𝑆 ) )
54	8 17 53	syl2anc	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m 𝑆 ) )
55		breq1	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( 𝑔 finSupp 0 ↔ ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 ) )
56		oveq1	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) )
57	56	eqeq1d	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
58	55 57	anbi12d	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) )
59		fveq1	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( 𝑔 ‘ 𝑠 ) = ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) )
60	59	neeq1d	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( ( 𝑔 ‘ 𝑠 ) ≠ 0 ↔ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 ) )
61	58 60	anbi12d	⊢ ( 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) → ( ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 ) ) )
62	61	adantl	⊢ ( ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) ∧ 𝑔 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ) → ( ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 ) ) )
63	54 62	rspcedv	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( ( ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑠 , ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) , ( 𝑓 ‘ 𝑧 ) ) ) ‘ 𝑠 ) ≠ 0 ) → ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
64	38 52 63	mp2and	⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
65	64	rexlimdva2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ 𝑠 ∈ 𝑆 ) → ( ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
66	65	reximdva	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
67	66	imp	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
68		df-3an	⊢ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
69		r19.42v	⊢ ( ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
70	68 69	bitr4i	⊢ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
71	70	rexbii	⊢ ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
72		rexcom	⊢ ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
73	71 72	bitri	⊢ ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
74	67 73	sylibr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
75	1 2 3 4 5	islindeps	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
76	75	3adant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
77	76	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
78	74 77	mpbird	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) ∧ ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) → 𝑆 linDepS 𝑀 )
79	78	ex	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → 𝑆 linDepS 𝑀 ) )