lsmsat

Description: Convert comparison of atom with sum of subspaces to a comparison to sum with atom. ( elpaddatiN analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	lsmsat.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsmsat.s	$⊢ S = LSubSp (W)$
	lsmsat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmsat.a	$⊢ A = LSAtoms (W)$
	lsmsat.w	$⊢ φ \to W \in LMod$
	lsmsat.t	$⊢ φ \to T \in S$
	lsmsat.u	$⊢ φ \to U \in S$
	lsmsat.q	$⊢ φ \to Q \in A$
	lsmsat.n	$⊢ φ \to T \neq \{\underset{˙}{0}\}$
	lsmsat.l	$⊢ φ \to Q \subseteq T \underset{˙}{\oplus} U$
Assertion	lsmsat	$⊢ φ \to \exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U)$

Proof

Step	Hyp	Ref	Expression
1		lsmsat.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lsmsat.s	$⊢ S = LSubSp (W)$
3		lsmsat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lsmsat.a	$⊢ A = LSAtoms (W)$
5		lsmsat.w	$⊢ φ \to W \in LMod$
6		lsmsat.t	$⊢ φ \to T \in S$
7		lsmsat.u	$⊢ φ \to U \in S$
8		lsmsat.q	$⊢ φ \to Q \in A$
9		lsmsat.n	$⊢ φ \to T \neq \{\underset{˙}{0}\}$
10		lsmsat.l	$⊢ φ \to Q \subseteq T \underset{˙}{\oplus} U$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12		eqid	$⊢ LSpan (W) = LSpan (W)$
13	11 12 1 4	islsat	$⊢ W \in LMod \to (Q \in A \leftrightarrow \exists r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{r\}))$
14	5 13	syl	$⊢ φ \to (Q \in A \leftrightarrow \exists r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{r\}))$
15	8 14	mpbid	$⊢ φ \to \exists r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{r\})$
16		simp3	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to Q = LSpan (W) (\{r\})$
17	10	3ad2ant1	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to Q \subseteq T \underset{˙}{\oplus} U$
18	16 17	eqsstrrd	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to LSpan (W) (\{r\}) \subseteq T \underset{˙}{\oplus} U$
19	5	3ad2ant1	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to W \in LMod$
20	2 3	lsmcl	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U \in S$
21	5 6 7 20	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U \in S$
22	21	3ad2ant1	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to T \underset{˙}{\oplus} U \in S$
23		eldifi	$⊢ r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to r \in {Base}_{W}$
24	23	3ad2ant2	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to r \in {Base}_{W}$
25	11 2 12 19 22 24	lspsnel5	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to (r \in (T \underset{˙}{\oplus} U) \leftrightarrow LSpan (W) (\{r\}) \subseteq T \underset{˙}{\oplus} U)$
26	18 25	mpbird	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to r \in (T \underset{˙}{\oplus} U)$
27	2	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
28	19 27	syl	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to S \subseteq SubGrp (W)$
29	6	3ad2ant1	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to T \in S$
30	28 29	sseldd	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to T \in SubGrp (W)$
31	7	3ad2ant1	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to U \in S$
32	28 31	sseldd	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to U \in SubGrp (W)$
33		eqid	$⊢ +_{W} = +_{W}$
34	33 3	lsmelval	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W)) \to (r \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U r = y +_{W} z)$
35	30 32 34	syl2anc	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to (r \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U r = y +_{W} z)$
36	26 35	mpbid	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to \exists y \in T \exists z \in U r = y +_{W} z$
37	1 2	lssne0	$⊢ T \in S \to (T \neq \{\underset{˙}{0}\} \leftrightarrow \exists q \in T q \neq \underset{˙}{0})$
38	6 37	syl	$⊢ φ \to (T \neq \{\underset{˙}{0}\} \leftrightarrow \exists q \in T q \neq \underset{˙}{0})$
39	9 38	mpbid	$⊢ φ \to \exists q \in T q \neq \underset{˙}{0}$
40	39	adantr	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to \exists q \in T q \neq \underset{˙}{0}$
41	40	3ad2ant1	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to \exists q \in T q \neq \underset{˙}{0}$
42	41	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y = \underset{˙}{0}) \to \exists q \in T q \neq \underset{˙}{0}$
43	5	adantr	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to W \in LMod$
44	43	3ad2ant1	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to W \in LMod$
45	44	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to W \in LMod$
46	6	adantr	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to T \in S$
47	46	3ad2ant1	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to T \in S$
48	47	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to T \in S$
49		simpr2	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to q \in T$
50	11 2	lssel	$⊢ (T \in S \land q \in T) \to q \in {Base}_{W}$
51	48 49 50	syl2anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to q \in {Base}_{W}$
52		simpr3	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to q \neq \underset{˙}{0}$
53	11 12 1 4	lsatlspsn2	$⊢ (W \in LMod \land q \in {Base}_{W} \land q \neq \underset{˙}{0}) \to LSpan (W) (\{q\}) \in A$
54	45 51 52 53	syl3anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{q\}) \in A$
55	2 12 45 48 49	lspsnel5a	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{q\}) \subseteq T$
56		simpl3	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to r = y +_{W} z$
57		simpr1	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to y = \underset{˙}{0}$
58	57	oveq1d	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to y +_{W} z = \underset{˙}{0} +_{W} z$
59	7	adantr	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to U \in S$
60	59	3ad2ant1	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to U \in S$
61		simp2r	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to z \in U$
62	11 2	lssel	$⊢ (U \in S \land z \in U) \to z \in {Base}_{W}$
63	60 61 62	syl2anc	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to z \in {Base}_{W}$
64	63	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to z \in {Base}_{W}$
65	11 33 1	lmod0vlid	$⊢ (W \in LMod \land z \in {Base}_{W}) \to \underset{˙}{0} +_{W} z = z$
66	45 64 65	syl2anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to \underset{˙}{0} +_{W} z = z$
67	56 58 66	3eqtrd	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to r = z$
68	67	sneqd	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to \{r\} = \{z\}$
69	68	fveq2d	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{r\}) = LSpan (W) (\{z\})$
70	2 12 44 60 61	lspsnel5a	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{z\}) \subseteq U$
71	70	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{z\}) \subseteq U$
72	69 71	eqsstrd	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{r\}) \subseteq U$
73	11 12	lspsnsubg	$⊢ (W \in LMod \land q \in {Base}_{W}) \to LSpan (W) (\{q\}) \in SubGrp (W)$
74	45 51 73	syl2anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{q\}) \in SubGrp (W)$
75	45 27	syl	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to S \subseteq SubGrp (W)$
76	60	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to U \in S$
77	75 76	sseldd	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to U \in SubGrp (W)$
78	3	lsmub2	$⊢ (LSpan (W) (\{q\}) \in SubGrp (W) \land U \in SubGrp (W)) \to U \subseteq LSpan (W) (\{q\}) \underset{˙}{\oplus} U$
79	74 77 78	syl2anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to U \subseteq LSpan (W) (\{q\}) \underset{˙}{\oplus} U$
80	72 79	sstrd	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to LSpan (W) (\{r\}) \subseteq LSpan (W) (\{q\}) \underset{˙}{\oplus} U$
81		sseq1	$⊢ p = LSpan (W) (\{q\}) \to (p \subseteq T \leftrightarrow LSpan (W) (\{q\}) \subseteq T)$
82		oveq1	$⊢ p = LSpan (W) (\{q\}) \to p \underset{˙}{\oplus} U = LSpan (W) (\{q\}) \underset{˙}{\oplus} U$
83	82	sseq2d	$⊢ p = LSpan (W) (\{q\}) \to (LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U \leftrightarrow LSpan (W) (\{r\}) \subseteq LSpan (W) (\{q\}) \underset{˙}{\oplus} U)$
84	81 83	anbi12d	$⊢ p = LSpan (W) (\{q\}) \to ((p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U) \leftrightarrow (LSpan (W) (\{q\}) \subseteq T \land LSpan (W) (\{r\}) \subseteq LSpan (W) (\{q\}) \underset{˙}{\oplus} U))$
85	84	rspcev	$⊢ (LSpan (W) (\{q\}) \in A \land (LSpan (W) (\{q\}) \subseteq T \land LSpan (W) (\{r\}) \subseteq LSpan (W) (\{q\}) \underset{˙}{\oplus} U)) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
86	54 55 80 85	syl12anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land (y = \underset{˙}{0} \land q \in T \land q \neq \underset{˙}{0})) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
87	86	3exp2	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to (y = \underset{˙}{0} \to (q \in T \to (q \neq \underset{˙}{0} \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))))$
88	87	imp	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y = \underset{˙}{0}) \to (q \in T \to (q \neq \underset{˙}{0} \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)))$
89	88	rexlimdv	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y = \underset{˙}{0}) \to (\exists q \in T q \neq \underset{˙}{0} \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))$
90	42 89	mpd	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y = \underset{˙}{0}) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
91	44	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to W \in LMod$
92		simp2l	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to y \in T$
93	11 2	lssel	$⊢ (T \in S \land y \in T) \to y \in {Base}_{W}$
94	47 92 93	syl2anc	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to y \in {Base}_{W}$
95	94	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to y \in {Base}_{W}$
96		simpr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to y \neq \underset{˙}{0}$
97	11 12 1 4	lsatlspsn2	$⊢ (W \in LMod \land y \in {Base}_{W} \land y \neq \underset{˙}{0}) \to LSpan (W) (\{y\}) \in A$
98	91 95 96 97	syl3anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to LSpan (W) (\{y\}) \in A$
99	2 12 44 47 92	lspsnel5a	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{y\}) \subseteq T$
100	99	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to LSpan (W) (\{y\}) \subseteq T$
101		simp3	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to r = y +_{W} z$
102	101	sneqd	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to \{r\} = \{y +_{W} z\}$
103	102	fveq2d	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{r\}) = LSpan (W) (\{y +_{W} z\})$
104	11 33 12	lspvadd	$⊢ (W \in LMod \land y \in {Base}_{W} \land z \in {Base}_{W}) \to LSpan (W) (\{y +_{W} z\}) \subseteq LSpan (W) (\{y, z\})$
105	44 94 63 104	syl3anc	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{y +_{W} z\}) \subseteq LSpan (W) (\{y, z\})$
106	103 105	eqsstrd	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y, z\})$
107	11 12 3 44 94 63	lsmpr	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{y, z\}) = LSpan (W) (\{y\}) \underset{˙}{\oplus} LSpan (W) (\{z\})$
108	106 107	sseqtrd	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} LSpan (W) (\{z\})$
109	44 27	syl	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to S \subseteq SubGrp (W)$
110	11 2 12	lspsncl	$⊢ (W \in LMod \land y \in {Base}_{W}) \to LSpan (W) (\{y\}) \in S$
111	44 94 110	syl2anc	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{y\}) \in S$
112	109 111	sseldd	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{y\}) \in SubGrp (W)$
113	109 60	sseldd	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to U \in SubGrp (W)$
114	3	lsmless2	$⊢ (LSpan (W) (\{y\}) \in SubGrp (W) \land U \in SubGrp (W) \land LSpan (W) (\{z\}) \subseteq U) \to LSpan (W) (\{y\}) \underset{˙}{\oplus} LSpan (W) (\{z\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U$
115	112 113 70 114	syl3anc	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{y\}) \underset{˙}{\oplus} LSpan (W) (\{z\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U$
116	108 115	sstrd	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U$
117	116	adantr	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U$
118		sseq1	$⊢ p = LSpan (W) (\{y\}) \to (p \subseteq T \leftrightarrow LSpan (W) (\{y\}) \subseteq T)$
119		oveq1	$⊢ p = LSpan (W) (\{y\}) \to p \underset{˙}{\oplus} U = LSpan (W) (\{y\}) \underset{˙}{\oplus} U$
120	119	sseq2d	$⊢ p = LSpan (W) (\{y\}) \to (LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U \leftrightarrow LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U)$
121	118 120	anbi12d	$⊢ p = LSpan (W) (\{y\}) \to ((p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U) \leftrightarrow (LSpan (W) (\{y\}) \subseteq T \land LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U))$
122	121	rspcev	$⊢ (LSpan (W) (\{y\}) \in A \land (LSpan (W) (\{y\}) \subseteq T \land LSpan (W) (\{r\}) \subseteq LSpan (W) (\{y\}) \underset{˙}{\oplus} U)) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
123	98 100 117 122	syl12anc	$⊢ (((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \land y \neq \underset{˙}{0}) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
124	90 123	pm2.61dane	$⊢ ((φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \land (y \in T \land z \in U) \land r = y +_{W} z) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
125	124	3exp	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to ((y \in T \land z \in U) \to (r = y +_{W} z \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)))$
126	125	rexlimdvv	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\})) \to (\exists y \in T \exists z \in U r = y +_{W} z \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))$
127	126	3adant3	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to (\exists y \in T \exists z \in U r = y +_{W} z \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))$
128	36 127	mpd	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
129		sseq1	$⊢ Q = LSpan (W) (\{r\}) \to (Q \subseteq p \underset{˙}{\oplus} U \leftrightarrow LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U)$
130	129	anbi2d	$⊢ Q = LSpan (W) (\{r\}) \to ((p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U) \leftrightarrow (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))$
131	130	rexbidv	$⊢ Q = LSpan (W) (\{r\}) \to (\exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U) \leftrightarrow \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))$
132	131	3ad2ant3	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to (\exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U) \leftrightarrow \exists p \in A (p \subseteq T \land LSpan (W) (\{r\}) \subseteq p \underset{˙}{\oplus} U))$
133	128 132	mpbird	$⊢ (φ \land r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \land Q = LSpan (W) (\{r\})) \to \exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U)$
134	133	3exp	$⊢ φ \to (r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) \to (Q = LSpan (W) (\{r\}) \to \exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U)))$
135	134	rexlimdv	$⊢ φ \to (\exists r \in ({Base}_{W} ∖ \{\underset{˙}{0}\}) Q = LSpan (W) (\{r\}) \to \exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U))$
136	15 135	mpd	$⊢ φ \to \exists p \in A (p \subseteq T \land Q \subseteq p \underset{˙}{\oplus} U)$

Metamath Proof Explorer

Theorem lsmsat

Proof