lsmelval2

Description: Subspace sum membership in terms of a sum of 1-dim subspaces (atoms), which can be useful for treating subspaces as projective lattice elements. (Contributed by NM, 9-Aug-2014)

	Ref	Expression
Hypotheses	lsmelval2.v	$⊢ V = {Base}_{W}$
	lsmelval2.s	$⊢ S = LSubSp (W)$
	lsmelval2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmelval2.n	$⊢ N = LSpan (W)$
	lsmelval2.w	$⊢ φ \to W \in LMod$
	lsmelval2.t	$⊢ φ \to T \in S$
	lsmelval2.u	$⊢ φ \to U \in S$
Assertion	lsmelval2	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow (X \in V \land \exists y \in T \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$

Proof

Step	Hyp	Ref	Expression
1		lsmelval2.v	$⊢ V = {Base}_{W}$
2		lsmelval2.s	$⊢ S = LSubSp (W)$
3		lsmelval2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lsmelval2.n	$⊢ N = LSpan (W)$
5		lsmelval2.w	$⊢ φ \to W \in LMod$
6		lsmelval2.t	$⊢ φ \to T \in S$
7		lsmelval2.u	$⊢ φ \to U \in S$
8	2	lsssubg	$⊢ (W \in LMod \land T \in S) \to T \in SubGrp (W)$
9	5 6 8	syl2anc	$⊢ φ \to T \in SubGrp (W)$
10	2	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
11	5 7 10	syl2anc	$⊢ φ \to U \in SubGrp (W)$
12		eqid	$⊢ +_{W} = +_{W}$
13	12 3	lsmelval	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W)) \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U X = y +_{W} z)$
14	9 11 13	syl2anc	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U X = y +_{W} z)$
15	5	adantr	$⊢ (φ \land (y \in T \land z \in U)) \to W \in LMod$
16	6	adantr	$⊢ (φ \land (y \in T \land z \in U)) \to T \in S$
17		simprl	$⊢ (φ \land (y \in T \land z \in U)) \to y \in T$
18	1 2	lssel	$⊢ (T \in S \land y \in T) \to y \in V$
19	16 17 18	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to y \in V$
20	1 2 4	lspsncl	$⊢ (W \in LMod \land y \in V) \to N (\{y\}) \in S$
21	15 19 20	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{y\}) \in S$
22	2	lsssubg	$⊢ (W \in LMod \land N (\{y\}) \in S) \to N (\{y\}) \in SubGrp (W)$
23	15 21 22	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{y\}) \in SubGrp (W)$
24	7	adantr	$⊢ (φ \land (y \in T \land z \in U)) \to U \in S$
25		simprr	$⊢ (φ \land (y \in T \land z \in U)) \to z \in U$
26	1 2	lssel	$⊢ (U \in S \land z \in U) \to z \in V$
27	24 25 26	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to z \in V$
28	1 2 4	lspsncl	$⊢ (W \in LMod \land z \in V) \to N (\{z\}) \in S$
29	15 27 28	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{z\}) \in S$
30	2	lsssubg	$⊢ (W \in LMod \land N (\{z\}) \in S) \to N (\{z\}) \in SubGrp (W)$
31	15 29 30	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{z\}) \in SubGrp (W)$
32	1 4	lspsnid	$⊢ (W \in LMod \land y \in V) \to y \in N (\{y\})$
33	15 19 32	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to y \in N (\{y\})$
34	1 4	lspsnid	$⊢ (W \in LMod \land z \in V) \to z \in N (\{z\})$
35	15 27 34	syl2anc	$⊢ (φ \land (y \in T \land z \in U)) \to z \in N (\{z\})$
36	12 3	lsmelvali	$⊢ ((N (\{y\}) \in SubGrp (W) \land N (\{z\}) \in SubGrp (W)) \land (y \in N (\{y\}) \land z \in N (\{z\}))) \to y +_{W} z \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\}))$
37	23 31 33 35 36	syl22anc	$⊢ (φ \land (y \in T \land z \in U)) \to y +_{W} z \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\}))$
38		eleq1a	$⊢ y +_{W} z \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \to (X = y +_{W} z \to X \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
39	37 38	syl	$⊢ (φ \land (y \in T \land z \in U)) \to (X = y +_{W} z \to X \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
40	2 3	lsmcl	$⊢ (W \in LMod \land N (\{y\}) \in S \land N (\{z\}) \in S) \to N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \in S$
41	15 21 29 40	syl3anc	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \in S$
42	1 2 4 15 41	lspsnel6	$⊢ (φ \land (y \in T \land z \in U)) \to (X \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \leftrightarrow (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
43	39 42	sylibd	$⊢ (φ \land (y \in T \land z \in U)) \to (X = y +_{W} z \to (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
44	43	reximdvva	$⊢ φ \to (\exists y \in T \exists z \in U X = y +_{W} z \to \exists y \in T \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
45	14 44	sylbid	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \to \exists y \in T \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
46	9	adantr	$⊢ (φ \land (y \in T \land z \in U)) \to T \in SubGrp (W)$
47	2 4 15 16 17	lspsnel5a	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{y\}) \subseteq T$
48	3	lsmless1	$⊢ (T \in SubGrp (W) \land N (\{z\}) \in SubGrp (W) \land N (\{y\}) \subseteq T) \to N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \subseteq T \underset{˙}{\oplus} N (\{z\})$
49	46 31 47 48	syl3anc	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \subseteq T \underset{˙}{\oplus} N (\{z\})$
50	11	adantr	$⊢ (φ \land (y \in T \land z \in U)) \to U \in SubGrp (W)$
51	2 4 15 24 25	lspsnel5a	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{z\}) \subseteq U$
52	3	lsmless2	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W) \land N (\{z\}) \subseteq U) \to T \underset{˙}{\oplus} N (\{z\}) \subseteq T \underset{˙}{\oplus} U$
53	46 50 51 52	syl3anc	$⊢ (φ \land (y \in T \land z \in U)) \to T \underset{˙}{\oplus} N (\{z\}) \subseteq T \underset{˙}{\oplus} U$
54	49 53	sstrd	$⊢ (φ \land (y \in T \land z \in U)) \to N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \subseteq T \underset{˙}{\oplus} U$
55	54	sseld	$⊢ (φ \land (y \in T \land z \in U)) \to (X \in (N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \to X \in (T \underset{˙}{\oplus} U))$
56	42 55	sylbird	$⊢ (φ \land (y \in T \land z \in U)) \to ((X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \to X \in (T \underset{˙}{\oplus} U))$
57	56	rexlimdvva	$⊢ φ \to (\exists y \in T \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \to X \in (T \underset{˙}{\oplus} U))$
58	45 57	impbid	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
59		r19.42v	$⊢ \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \leftrightarrow (X \in V \land \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}))$
60	59	rexbii	$⊢ \exists y \in T \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \leftrightarrow \exists y \in T (X \in V \land \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}))$
61		r19.42v	$⊢ \exists y \in T (X \in V \land \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \leftrightarrow (X \in V \land \exists y \in T \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}))$
62	60 61	bitri	$⊢ \exists y \in T \exists z \in U (X \in V \land N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \leftrightarrow (X \in V \land \exists y \in T \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}))$
63	58 62	bitrdi	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow (X \in V \land \exists y \in T \exists z \in U N (\{X\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$

Metamath Proof Explorer

Theorem lsmelval2

Proof