Metamath Proof Explorer

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 𝑀 ) )