Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldepsnlinc Structured version   Visualization version   GIF version

Theorem ldepsnlinc 42898
Description: The reverse implication of islindeps2 42873 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 combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 42886 and zlmodzxznm 42887. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
Assertion
Ref Expression
ldepsnlinc 𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣))
Distinct variable group:   𝑓,𝑚,𝑠,𝑣

Proof of Theorem ldepsnlinc
StepHypRef Expression
1 eqid 2764 . . . 4 (ℤring freeLMod {0, 1}) = (ℤring freeLMod {0, 1})
21zlmodzxzlmod 42733 . . 3 ((ℤring freeLMod {0, 1}) ∈ LMod ∧ ℤring = (Scalar‘(ℤring freeLMod {0, 1})))
32simpli 476 . 2 (ℤring freeLMod {0, 1}) ∈ LMod
4 3z 11656 . . . . 5 3 ∈ ℤ
5 6nn 11363 . . . . . 6 6 ∈ ℕ
65nnzi 11647 . . . . 5 6 ∈ ℤ
71zlmodzxzel 42734 . . . . 5 ((3 ∈ ℤ ∧ 6 ∈ ℤ) → {⟨0, 3⟩, ⟨1, 6⟩} ∈ (Base‘(ℤring freeLMod {0, 1})))
84, 6, 7mp2an 683 . . . 4 {⟨0, 3⟩, ⟨1, 6⟩} ∈ (Base‘(ℤring freeLMod {0, 1}))
9 2z 11655 . . . . 5 2 ∈ ℤ
10 4z 11657 . . . . 5 4 ∈ ℤ
111zlmodzxzel 42734 . . . . 5 ((2 ∈ ℤ ∧ 4 ∈ ℤ) → {⟨0, 2⟩, ⟨1, 4⟩} ∈ (Base‘(ℤring freeLMod {0, 1})))
129, 10, 11mp2an 683 . . . 4 {⟨0, 2⟩, ⟨1, 4⟩} ∈ (Base‘(ℤring freeLMod {0, 1}))
13 prelpwi 5070 . . . 4 (({⟨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})))
148, 12, 13mp2an 683 . . 3 {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∈ 𝒫 (Base‘(ℤring freeLMod {0, 1}))
15 eqid 2764 . . . . 5 {⟨0, 3⟩, ⟨1, 6⟩} = {⟨0, 3⟩, ⟨1, 6⟩}
16 eqid 2764 . . . . 5 {⟨0, 2⟩, ⟨1, 4⟩} = {⟨0, 2⟩, ⟨1, 4⟩}
171, 15, 16zlmodzxzldep 42894 . . . 4 {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} linDepS (ℤring freeLMod {0, 1})
181, 15, 16ldepsnlinclem1 42895 . . . . . . . 8 (𝑓 ∈ ((Base‘ℤring) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}}) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 2⟩, ⟨1, 4⟩}}) ≠ {⟨0, 3⟩, ⟨1, 6⟩})
19 simpr 477 . . . . . . . . . . . 12 (((ℤring freeLMod {0, 1}) ∈ LMod ∧ ℤring = (Scalar‘(ℤring freeLMod {0, 1}))) → ℤring = (Scalar‘(ℤring freeLMod {0, 1})))
2019eqcomd 2770 . . . . . . . . . . 11 (((ℤring freeLMod {0, 1}) ∈ LMod ∧ ℤring = (Scalar‘(ℤring freeLMod {0, 1}))) → (Scalar‘(ℤring freeLMod {0, 1})) = ℤring)
212, 20ax-mp 5 . . . . . . . . . 10 (Scalar‘(ℤring freeLMod {0, 1})) = ℤring
2221fveq2i 6377 . . . . . . . . 9 (Base‘(Scalar‘(ℤring freeLMod {0, 1}))) = (Base‘ℤring)
2322oveq1i 6851 . . . . . . . 8 ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}}) = ((Base‘ℤring) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}})
2418, 23eleq2s 2861 . . . . . . 7 (𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}}) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 2⟩, ⟨1, 4⟩}}) ≠ {⟨0, 3⟩, ⟨1, 6⟩})
2524a1d 25 . . . . . 6 (𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}}) → (𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 2⟩, ⟨1, 4⟩}}) ≠ {⟨0, 3⟩, ⟨1, 6⟩}))
2625rgen 3068 . . . . 5 𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}})(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 2⟩, ⟨1, 4⟩}}) ≠ {⟨0, 3⟩, ⟨1, 6⟩})
271, 15, 16ldepsnlinclem2 42896 . . . . . . . 8 (𝑓 ∈ ((Base‘ℤring) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}}) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 3⟩, ⟨1, 6⟩}}) ≠ {⟨0, 2⟩, ⟨1, 4⟩})
2822oveq1i 6851 . . . . . . . 8 ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}}) = ((Base‘ℤring) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}})
2927, 28eleq2s 2861 . . . . . . 7 (𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}}) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 3⟩, ⟨1, 6⟩}}) ≠ {⟨0, 2⟩, ⟨1, 4⟩})
3029a1d 25 . . . . . 6 (𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}}) → (𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 3⟩, ⟨1, 6⟩}}) ≠ {⟨0, 2⟩, ⟨1, 4⟩}))
3130rgen 3068 . . . . 5 𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨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 5064 . . . . . 6 {⟨0, 3⟩, ⟨1, 6⟩} ∈ V
33 prex 5064 . . . . . 6 {⟨0, 2⟩, ⟨1, 4⟩} ∈ V
34 sneq 4343 . . . . . . . . . 10 (𝑣 = {⟨0, 3⟩, ⟨1, 6⟩} → {𝑣} = {{⟨0, 3⟩, ⟨1, 6⟩}})
3534difeq2d 3889 . . . . . . . . 9 (𝑣 = {⟨0, 3⟩, ⟨1, 6⟩} → ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣}) = ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {{⟨0, 3⟩, ⟨1, 6⟩}}))
361, 15, 16zlmodzxzldeplem 42888 . . . . . . . . . 10 {⟨0, 3⟩, ⟨1, 6⟩} ≠ {⟨0, 2⟩, ⟨1, 4⟩}
37 difprsn1 4484 . . . . . . . . . 10 ({⟨0, 3⟩, ⟨1, 6⟩} ≠ {⟨0, 2⟩, ⟨1, 4⟩} → ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {{⟨0, 3⟩, ⟨1, 6⟩}}) = {{⟨0, 2⟩, ⟨1, 4⟩}})
3836, 37ax-mp 5 . . . . . . . . 9 ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {{⟨0, 3⟩, ⟨1, 6⟩}}) = {{⟨0, 2⟩, ⟨1, 4⟩}}
3935, 38syl6eq 2814 . . . . . . . 8 (𝑣 = {⟨0, 3⟩, ⟨1, 6⟩} → ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣}) = {{⟨0, 2⟩, ⟨1, 4⟩}})
4039oveq2d 6857 . . . . . . 7 (𝑣 = {⟨0, 3⟩, ⟨1, 6⟩} → ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣})) = ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 2⟩, ⟨1, 4⟩}}))
4139oveq2d 6857 . . . . . . . . 9 (𝑣 = {⟨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 22 . . . . . . . . 9 (𝑣 = {⟨0, 3⟩, ⟨1, 6⟩} → 𝑣 = {⟨0, 3⟩, ⟨1, 6⟩})
4341, 42neeq12d 2997 . . . . . . . 8 (𝑣 = {⟨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⟩}))
4443imbi2d 331 . . . . . . 7 (𝑣 = {⟨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⟩})))
4540, 44raleqbidv 3299 . . . . . 6 (𝑣 = {⟨0, 3⟩, ⟨1, 6⟩} → (∀𝑓 ∈ ((Base‘(Scalar‘(ℤ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⟩}} ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨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 4343 . . . . . . . . . 10 (𝑣 = {⟨0, 2⟩, ⟨1, 4⟩} → {𝑣} = {{⟨0, 2⟩, ⟨1, 4⟩}})
4746difeq2d 3889 . . . . . . . . 9 (𝑣 = {⟨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 4485 . . . . . . . . . 10 ({⟨0, 3⟩, ⟨1, 6⟩} ≠ {⟨0, 2⟩, ⟨1, 4⟩} → ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {{⟨0, 2⟩, ⟨1, 4⟩}}) = {{⟨0, 3⟩, ⟨1, 6⟩}})
4936, 48ax-mp 5 . . . . . . . . 9 ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {{⟨0, 2⟩, ⟨1, 4⟩}}) = {{⟨0, 3⟩, ⟨1, 6⟩}}
5047, 49syl6eq 2814 . . . . . . . 8 (𝑣 = {⟨0, 2⟩, ⟨1, 4⟩} → ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣}) = {{⟨0, 3⟩, ⟨1, 6⟩}})
5150oveq2d 6857 . . . . . . 7 (𝑣 = {⟨0, 2⟩, ⟨1, 4⟩} → ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣})) = ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}}))
5250oveq2d 6857 . . . . . . . . 9 (𝑣 = {⟨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 22 . . . . . . . . 9 (𝑣 = {⟨0, 2⟩, ⟨1, 4⟩} → 𝑣 = {⟨0, 2⟩, ⟨1, 4⟩})
5452, 53neeq12d 2997 . . . . . . . 8 (𝑣 = {⟨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⟩}))
5554imbi2d 331 . . . . . . 7 (𝑣 = {⟨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⟩})))
5651, 55raleqbidv 3299 . . . . . 6 (𝑣 = {⟨0, 2⟩, ⟨1, 4⟩} → (∀𝑓 ∈ ((Base‘(Scalar‘(ℤ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⟩}} ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}})(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 3⟩, ⟨1, 6⟩}}) ≠ {⟨0, 2⟩, ⟨1, 4⟩})))
5732, 33, 45, 56ralpr 4393 . . . . 5 (∀𝑣 ∈ {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}}∀𝑓 ∈ ((Base‘(Scalar‘(ℤ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⟩}} ∖ {𝑣})) ≠ 𝑣) ↔ (∀𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 {{⟨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}))) ↑𝑚 {{⟨0, 3⟩, ⟨1, 6⟩}})(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1})){{⟨0, 3⟩, ⟨1, 6⟩}}) ≠ {⟨0, 2⟩, ⟨1, 4⟩})))
5826, 31, 57mpbir2an 702 . . . 4 𝑣 ∈ {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}}∀𝑓 ∈ ((Base‘(Scalar‘(ℤ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⟩}} ∖ {𝑣})) ≠ 𝑣)
5917, 58pm3.2i 462 . . 3 ({{⟨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}))) ↑𝑚 ({{⟨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 4811 . . . . 5 (𝑠 = {{⟨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 22 . . . . . 6 (𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} → 𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}})
62 difeq1 3882 . . . . . . . 8 (𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} → (𝑠 ∖ {𝑣}) = ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣}))
6362oveq2d 6857 . . . . . . 7 (𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} → ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣})) = ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 ({{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} ∖ {𝑣})))
6462oveq2d 6857 . . . . . . . . 9 (𝑠 = {{⟨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⟩}} ∖ {𝑣})))
6564neeq1d 2995 . . . . . . . 8 (𝑠 = {{⟨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⟩}} ∖ {𝑣})) ≠ 𝑣))
6665imbi2d 331 . . . . . . 7 (𝑠 = {{⟨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⟩}} ∖ {𝑣})) ≠ 𝑣)))
6763, 66raleqbidv 3299 . . . . . 6 (𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} → (∀𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈ ((Base‘(Scalar‘(ℤ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⟩}} ∖ {𝑣})) ≠ 𝑣)))
6861, 67raleqbidv 3299 . . . . 5 (𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} → (∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 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}))) ↑𝑚 ({{⟨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⟩}} ∖ {𝑣})) ≠ 𝑣)))
6960, 68anbi12d 624 . . . 4 (𝑠 = {{⟨0, 3⟩, ⟨1, 6⟩}, {⟨0, 2⟩, ⟨1, 4⟩}} → ((𝑠 linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 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}))) ↑𝑚 ({{⟨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⟩}} ∖ {𝑣})) ≠ 𝑣))))
7069rspcev 3460 . . 3 (({{⟨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}))) ↑𝑚 ({{⟨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}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)))
7114, 59, 70mp2an 683 . 2 𝑠 ∈ 𝒫 (Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))
72 fveq2 6374 . . . . 5 (𝑚 = (ℤring freeLMod {0, 1}) → (Base‘𝑚) = (Base‘(ℤring freeLMod {0, 1})))
7372pweqd 4319 . . . 4 (𝑚 = (ℤring freeLMod {0, 1}) → 𝒫 (Base‘𝑚) = 𝒫 (Base‘(ℤring freeLMod {0, 1})))
74 breq2 4812 . . . . 5 (𝑚 = (ℤring freeLMod {0, 1}) → (𝑠 linDepS 𝑚𝑠 linDepS (ℤring freeLMod {0, 1})))
75 2fveq3 6379 . . . . . . . 8 (𝑚 = (ℤring freeLMod {0, 1}) → (Base‘(Scalar‘𝑚)) = (Base‘(Scalar‘(ℤring freeLMod {0, 1}))))
7675oveq1d 6856 . . . . . . 7 (𝑚 = (ℤring freeLMod {0, 1}) → ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣})) = ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣})))
77 2fveq3 6379 . . . . . . . . 9 (𝑚 = (ℤring freeLMod {0, 1}) → (0g‘(Scalar‘𝑚)) = (0g‘(Scalar‘(ℤring freeLMod {0, 1}))))
7877breq2d 4820 . . . . . . . 8 (𝑚 = (ℤring freeLMod {0, 1}) → (𝑓 finSupp (0g‘(Scalar‘𝑚)) ↔ 𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1})))))
79 fveq2 6374 . . . . . . . . . 10 (𝑚 = (ℤring freeLMod {0, 1}) → ( linC ‘𝑚) = ( linC ‘(ℤring freeLMod {0, 1})))
8079oveqd 6858 . . . . . . . . 9 (𝑚 = (ℤring freeLMod {0, 1}) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})))
8180neeq1d 2995 . . . . . . . 8 (𝑚 = (ℤring freeLMod {0, 1}) → ((𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣 ↔ (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))
8278, 81imbi12d 335 . . . . . . 7 (𝑚 = (ℤring freeLMod {0, 1}) → ((𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ (𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)))
8376, 82raleqbidv 3299 . . . . . 6 (𝑚 = (ℤring freeLMod {0, 1}) → (∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)))
8483ralbidv 3132 . . . . 5 (𝑚 = (ℤring freeLMod {0, 1}) → (∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)))
8574, 84anbi12d 624 . . . 4 (𝑚 = (ℤring freeLMod {0, 1}) → ((𝑠 linDepS 𝑚 ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) ↔ (𝑠 linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))))
8673, 85rexeqbidv 3300 . . 3 (𝑚 = (ℤring freeLMod {0, 1}) → (∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) ↔ ∃𝑠 ∈ 𝒫 (Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))))
8786rspcev 3460 . 2 (((ℤring freeLMod {0, 1}) ∈ LMod ∧ ∃𝑠 ∈ 𝒫 (Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1}))) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘(ℤring freeLMod {0, 1}))) → (𝑓( linC ‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))) → ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)))
883, 71, 87mp2an 683 1 𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣𝑠𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wne 2936  wral 3054  wrex 3055  cdif 3728  𝒫 cpw 4314  {csn 4333  {cpr 4335  cop 4339   class class class wbr 4808  cfv 6067  (class class class)co 6841  𝑚 cmap 8059   finSupp cfsupp 8481  0cc0 10188  1c1 10189  2c2 11326  3c3 11327  4c4 11328  6c6 11330  cz 11623  Basecbs 16131  Scalarcsca 16218  0gc0g 16367  LModclmod 19131  ringzring 20090   freeLMod cfrlm 20365   linC clinc 42794   linDepS clindeps 42831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-rp 12028  df-fz 12533  df-fzo 12673  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-dvds 15267  df-prm 15667  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-starv 16230  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-unif 16238  df-hom 16239  df-cco 16240  df-0g 16369  df-gsum 16370  df-prds 16375  df-pws 16377  df-mre 16513  df-mrc 16514  df-acs 16516  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-submnd 17603  df-grp 17693  df-minusg 17694  df-sbg 17695  df-mulg 17809  df-subg 17856  df-cntz 18014  df-cmn 18460  df-abl 18461  df-mgp 18756  df-ur 18768  df-ring 18815  df-cring 18816  df-subrg 19046  df-lmod 19133  df-lss 19201  df-sra 19445  df-rgmod 19446  df-cnfld 20019  df-zring 20091  df-dsmm 20351  df-frlm 20366  df-linc 42796  df-lininds 42832  df-lindeps 42834
This theorem is referenced by:  ldepslinc  42899
  Copyright terms: Public domain W3C validator