Metamath Proof Explorer

Theorem ldepsnlinc

Description: The reverse implication of islindeps2 does not hold for arbitrary (left) modules, see note in Roman p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combination of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa and zlmodzxznm . (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Assertion ldepsnlinc ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ℤring freeLMod { 0 , 1 } ) = ( ℤring freeLMod { 0 , 1 } )
2 1 zlmodzxzlmod ⊢ ( ( ℤring freeLMod { 0 , 1 } ) ∈ LMod ∧ ℤring = ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
3 2 simpli ⊢ ( ℤring freeLMod { 0 , 1 } ) ∈ LMod
4 3z ⊢ 3 ∈ ℤ
5 6nn ⊢ 6 ∈ ℕ
6 5 nnzi ⊢ 6 ∈ ℤ
7 1 zlmodzxzel ⊢ ( ( 3 ∈ ℤ ∧ 6 ∈ ℤ ) → { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
8 4 6 7 mp2an ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) )
9 2z ⊢ 2 ∈ ℤ
10 4z ⊢ 4 ∈ ℤ
11 1 zlmodzxzel ⊢ ( ( 2 ∈ ℤ ∧ 4 ∈ ℤ ) → { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
12 9 10 11 mp2an ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) )
13 prelpwi ⊢ ( ( { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ∧ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
14 8 12 13 mp2an ⊢ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) )
15 eqid ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
16 eqid ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
17 1 15 16 zlmodzxzldep ⊢ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } linDepS ( ℤring freeLMod { 0 , 1 } )
18 1 15 16 ldepsnlinclem1 ⊢ ( 𝑓 ∈ ( ( Base ‘ ℤring ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
19 simpr ⊢ ( ( ( ℤring freeLMod { 0 , 1 } ) ∈ LMod ∧ ℤring = ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ℤring = ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
20 19 eqcomd ⊢ ( ( ( ℤring freeLMod { 0 , 1 } ) ∈ LMod ∧ ℤring = ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) = ℤring )
21 2 20 ax-mp ⊢ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) = ℤring
22 21 fveq2i ⊢ ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) = ( Base ‘ ℤring )
23 22 oveq1i ⊢ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) = ( ( Base ‘ ℤring ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } )
24 18 23 eleq2s ⊢ ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
25 24 a1d ⊢ ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) → ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) )
26 25 rgen ⊢ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
27 1 15 16 ldepsnlinclem2 ⊢ ( 𝑓 ∈ ( ( Base ‘ ℤring ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
28 22 oveq1i ⊢ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) = ( ( Base ‘ ℤring ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } )
29 27 28 eleq2s ⊢ ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
30 29 a1d ⊢ ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) → ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) )
31 30 rgen ⊢ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
32 prex ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ V
33 prex ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ V
34 sneq ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → { 𝑣 } = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } )
35 34 difeq2d ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) = ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) )
36 1 15 16 zlmodzxzldeplem ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
37 difprsn1 ⊢ ( { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) = { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } )
38 36 37 ax-mp ⊢ ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) = { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } }
39 35 38 eqtrdi ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) = { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } )
40 39 oveq2d ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) = ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) )
41 39 oveq2d ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) = ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) )
42 id ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
43 41 42 neeq12d ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ↔ ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) )
44 43 imbi2d ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) ) )
45 40 44 raleqbidv ⊢ ( 𝑣 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } → ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) ) )
46 sneq ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → { 𝑣 } = { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } )
47 46 difeq2d ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) = ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) )
48 difprsn2 ⊢ ( { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } )
49 36 48 ax-mp ⊢ ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } }
50 47 49 eqtrdi ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } )
51 50 oveq2d ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) = ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) )
52 50 oveq2d ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) = ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) )
53 id ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
54 52 53 neeq12d ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ↔ ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) )
55 54 imbi2d ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) ) )
56 51 55 raleqbidv ⊢ ( 𝑣 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } → ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) ) )
57 32 33 45 56 ralpr ⊢ ( ∀ 𝑣 ∈ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ) ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } } ) ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) ) )
58 26 31 57 mpbir2an ⊢ ∀ 𝑣 ∈ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 )
59 17 58 pm3.2i ⊢ ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) )
60 breq1 ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ↔ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } linDepS ( ℤring freeLMod { 0 , 1 } ) ) )
61 id ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } )
62 difeq1 ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( 𝑠 ∖ { 𝑣 } ) = ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) )
63 62 oveq2d ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) = ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) )
64 62 oveq2d ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) = ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) )
65 64 neeq1d ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ↔ ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) )
66 65 imbi2d ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
67 63 66 raleqbidv ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
68 61 67 raleqbidv ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑣 ∈ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
69 60 68 anbi12d ⊢ ( 𝑠 = { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } → ( ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ↔ ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ) )
70 69 rspcev ⊢ ( ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ∧ ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( { { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } , { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } } ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ) → ∃ 𝑠 ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
71 14 59 70 mp2an ⊢ ∃ 𝑠 ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) )
72 fveq2 ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( Base ‘ 𝑚 ) = ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
73 72 pweqd ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → 𝒫 ( Base ‘ 𝑚 ) = 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
74 breq2 ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( 𝑠 linDepS 𝑚 ↔ 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ) )
75 2fveq3 ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) )
76 75 oveq1d ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) = ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) )
77 2fveq3 ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) )
78 77 breq2d ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ↔ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ) )
79 fveq2 ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( linC ‘ 𝑚 ) = ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) )
80 79 oveqd ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) = ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) )
81 80 neeq1d ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ↔ ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) )
82 78 81 imbi12d ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
83 76 82 raleqbidv ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
84 83 ralbidv ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ↔ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
85 74 84 anbi12d ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ↔ ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ) )
86 73 85 rexeqbidv ⊢ ( 𝑚 = ( ℤring freeLMod { 0 , 1 } ) → ( ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ↔ ∃ 𝑠 ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ) )
87 86 rspcev ⊢ ( ( ( ℤring freeLMod { 0 , 1 } ) ∈ LMod ∧ ∃ 𝑠 ∈ 𝒫 ( Base ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 linDepS ( ℤring freeLMod { 0 , 1 } ) ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ ( ℤring freeLMod { 0 , 1 } ) ) ) → ( 𝑓 ( linC ‘ ( ℤring freeLMod { 0 , 1 } ) ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) ) → ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) ) )
88 3 71 87 mp2an ⊢ ∃ 𝑚 ∈ LMod ∃ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ( 𝑠 linDepS 𝑚 ∧ ∀ 𝑣 ∈ 𝑠 ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m ( 𝑠 ∖ { 𝑣 } ) ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) → ( 𝑓 ( linC ‘ 𝑚 ) ( 𝑠 ∖ { 𝑣 } ) ) ≠ 𝑣 ) )