Definition df-lininds 42025

Description: Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.)

Assertion

Ref	Expression
df-lininds	⊢ linIndS = {⟨𝑠, 𝑚⟩ ∣ (𝑠 ∈ 𝒫 (Base‘𝑚) ∧ ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))}

Distinct variable group:   𝑓,𝑚,𝑠,𝑥

Detailed syntax breakdown of Definition df-lininds

Step	Hyp	Ref	Expression
1		clininds 42023	. 2 class linIndS
2		vs	. . . . . 6 setvar 𝑠
3	2	cv 1474	. . . . 5 class 𝑠
4		vm	. . . . . . . 8 setvar 𝑚
5	4	cv 1474	. . . . . . 7 class 𝑚
6		cbs 15695	. . . . . . 7 class Base
7	5, 6	cfv 5804	. . . . . 6 class (Base‘𝑚)
8	7	cpw 4108	. . . . 5 class 𝒫 (Base‘𝑚)
9	3, 8	wcel 1977	. . . 4 wff 𝑠 ∈ 𝒫 (Base‘𝑚)
10		vf	. . . . . . . . 9 setvar 𝑓
11	10	cv 1474	. . . . . . . 8 class 𝑓
12		csca 15771	. . . . . . . . . 10 class Scalar
13	5, 12	cfv 5804	. . . . . . . . 9 class (Scalar‘𝑚)
14		c0g 15923	. . . . . . . . 9 class 0g
15	13, 14	cfv 5804	. . . . . . . 8 class (0g‘(Scalar‘𝑚))
16		cfsupp 8158	. . . . . . . 8 class finSupp
17	11, 15, 16	wbr 4583	. . . . . . 7 wff 𝑓 finSupp (0g‘(Scalar‘𝑚))
18		clinc 41987	. . . . . . . . . 10 class linC
19	5, 18	cfv 5804	. . . . . . . . 9 class ( linC ‘𝑚)
20	11, 3, 19	co 6549	. . . . . . . 8 class (𝑓( linC ‘𝑚)𝑠)
21	5, 14	cfv 5804	. . . . . . . 8 class (0g‘𝑚)
22	20, 21	wceq 1475	. . . . . . 7 wff (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)
23	17, 22	wa 383	. . . . . 6 wff (𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚))
24		vx	. . . . . . . . . 10 setvar 𝑥
25	24	cv 1474	. . . . . . . . 9 class 𝑥
26	25, 11	cfv 5804	. . . . . . . 8 class (𝑓‘𝑥)
27	26, 15	wceq 1475	. . . . . . 7 wff (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))
28	27, 24, 3	wral 2896	. . . . . 6 wff ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))
29	23, 28	wi 4	. . . . 5 wff ((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚)))
30	13, 6	cfv 5804	. . . . . 6 class (Base‘(Scalar‘𝑚))
31		cmap 7744	. . . . . 6 class ↑𝑚
32	30, 3, 31	co 6549	. . . . 5 class ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)
33	29, 10, 32	wral 2896	. . . 4 wff ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚)))
34	9, 33	wa 383	. . 3 wff (𝑠 ∈ 𝒫 (Base‘𝑚) ∧ ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))
35	34, 2, 4	copab 4642	. 2 class {⟨𝑠, 𝑚⟩ ∣ (𝑠 ∈ 𝒫 (Base‘𝑚) ∧ ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))}
36	1, 35	wceq 1475	1 wff linIndS = {⟨𝑠, 𝑚⟩ ∣ (𝑠 ∈ 𝒫 (Base‘𝑚) ∧ ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))}

This definition is referenced by:  rellininds  42026  islininds  42029