lsmspsn

Description: Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015)

	Ref	Expression
Hypotheses	lsmspsn.v	$⊢ V = {Base}_{W}$
	lsmspsn.a	$⊢ \underset{˙}{+} = +_{W}$
	lsmspsn.f	$⊢ F = Scalar (W)$
	lsmspsn.k	$⊢ K = {Base}_{F}$
	lsmspsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lsmspsn.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmspsn.n	$⊢ N = LSpan (W)$
	lsmspsn.w	$⊢ φ \to W \in LMod$
	lsmspsn.x	$⊢ φ \to X \in V$
	lsmspsn.y	$⊢ φ \to Y \in V$
Assertion	lsmspsn	$⊢ φ \to (U \in (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \leftrightarrow \exists j \in K \exists k \in K U = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y))$

Proof

Step	Hyp	Ref	Expression
1		lsmspsn.v	$⊢ V = {Base}_{W}$
2		lsmspsn.a	$⊢ \underset{˙}{+} = +_{W}$
3		lsmspsn.f	$⊢ F = Scalar (W)$
4		lsmspsn.k	$⊢ K = {Base}_{F}$
5		lsmspsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lsmspsn.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
7		lsmspsn.n	$⊢ N = LSpan (W)$
8		lsmspsn.w	$⊢ φ \to W \in LMod$
9		lsmspsn.x	$⊢ φ \to X \in V$
10		lsmspsn.y	$⊢ φ \to Y \in V$
11	1 7	lspsnsubg	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in SubGrp (W)$
12	8 9 11	syl2anc	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
13	1 7	lspsnsubg	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in SubGrp (W)$
14	8 10 13	syl2anc	$⊢ φ \to N (\{Y\}) \in SubGrp (W)$
15	2 6	lsmelval	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{Y\}) \in SubGrp (W)) \to (U \in (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \leftrightarrow \exists v \in N (\{X\}) \exists w \in N (\{Y\}) U = v \underset{˙}{+} w)$
16	12 14 15	syl2anc	$⊢ φ \to (U \in (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \leftrightarrow \exists v \in N (\{X\}) \exists w \in N (\{Y\}) U = v \underset{˙}{+} w)$
17	3 4 1 5 7	ellspsn	$⊢ (W \in LMod \land X \in V) \to (v \in N (\{X\}) \leftrightarrow \exists j \in K v = j \underset{˙}{\cdot} X)$
18	8 9 17	syl2anc	$⊢ φ \to (v \in N (\{X\}) \leftrightarrow \exists j \in K v = j \underset{˙}{\cdot} X)$
19	3 4 1 5 7	ellspsn	$⊢ (W \in LMod \land Y \in V) \to (w \in N (\{Y\}) \leftrightarrow \exists k \in K w = k \underset{˙}{\cdot} Y)$
20	8 10 19	syl2anc	$⊢ φ \to (w \in N (\{Y\}) \leftrightarrow \exists k \in K w = k \underset{˙}{\cdot} Y)$
21	18 20	anbi12d	$⊢ φ \to ((v \in N (\{X\}) \land w \in N (\{Y\})) \leftrightarrow (\exists j \in K v = j \underset{˙}{\cdot} X \land \exists k \in K w = k \underset{˙}{\cdot} Y))$
22	21	biimpa	$⊢ (φ \land (v \in N (\{X\}) \land w \in N (\{Y\}))) \to (\exists j \in K v = j \underset{˙}{\cdot} X \land \exists k \in K w = k \underset{˙}{\cdot} Y)$
23	22	biantrurd	$⊢ (φ \land (v \in N (\{X\}) \land w \in N (\{Y\}))) \to (U = v \underset{˙}{+} w \leftrightarrow ((\exists j \in K v = j \underset{˙}{\cdot} X \land \exists k \in K w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w))$
24		r19.41v	$⊢ \exists k \in K ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow (\exists k \in K (v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w)$
25	24	rexbii	$⊢ \exists j \in K \exists k \in K ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow \exists j \in K (\exists k \in K (v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w)$
26		r19.41v	$⊢ \exists j \in K (\exists k \in K (v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow (\exists j \in K \exists k \in K (v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w)$
27		reeanv	$⊢ \exists j \in K \exists k \in K (v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \leftrightarrow (\exists j \in K v = j \underset{˙}{\cdot} X \land \exists k \in K w = k \underset{˙}{\cdot} Y)$
28	27	anbi1i	$⊢ (\exists j \in K \exists k \in K (v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow ((\exists j \in K v = j \underset{˙}{\cdot} X \land \exists k \in K w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w)$
29	25 26 28	3bitrri	$⊢ ((\exists j \in K v = j \underset{˙}{\cdot} X \land \exists k \in K w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow \exists j \in K \exists k \in K ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w)$
30	23 29	bitrdi	$⊢ (φ \land (v \in N (\{X\}) \land w \in N (\{Y\}))) \to (U = v \underset{˙}{+} w \leftrightarrow \exists j \in K \exists k \in K ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w))$
31	30	2rexbidva	$⊢ φ \to (\exists v \in N (\{X\}) \exists w \in N (\{Y\}) U = v \underset{˙}{+} w \leftrightarrow \exists v \in N (\{X\}) \exists w \in N (\{Y\}) \exists j \in K \exists k \in K ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w))$
32		rexrot4	$⊢ \exists v \in N (\{X\}) \exists w \in N (\{Y\}) \exists j \in K \exists k \in K ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow \exists j \in K \exists k \in K \exists v \in N (\{X\}) \exists w \in N (\{Y\}) ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w)$
33	31 32	bitrdi	$⊢ φ \to (\exists v \in N (\{X\}) \exists w \in N (\{Y\}) U = v \underset{˙}{+} w \leftrightarrow \exists j \in K \exists k \in K \exists v \in N (\{X\}) \exists w \in N (\{Y\}) ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w))$
34	8	adantr	$⊢ (φ \land (j \in K \land k \in K)) \to W \in LMod$
35		simprl	$⊢ (φ \land (j \in K \land k \in K)) \to j \in K$
36	9	adantr	$⊢ (φ \land (j \in K \land k \in K)) \to X \in V$
37	1 5 3 4 7 34 35 36	ellspsni	$⊢ (φ \land (j \in K \land k \in K)) \to j \underset{˙}{\cdot} X \in N (\{X\})$
38		simprr	$⊢ (φ \land (j \in K \land k \in K)) \to k \in K$
39	10	adantr	$⊢ (φ \land (j \in K \land k \in K)) \to Y \in V$
40	1 5 3 4 7 34 38 39	ellspsni	$⊢ (φ \land (j \in K \land k \in K)) \to k \underset{˙}{\cdot} Y \in N (\{Y\})$
41		oveq1	$⊢ v = j \underset{˙}{\cdot} X \to v \underset{˙}{+} w = (j \underset{˙}{\cdot} X) \underset{˙}{+} w$
42	41	eqeq2d	$⊢ v = j \underset{˙}{\cdot} X \to (U = v \underset{˙}{+} w \leftrightarrow U = (j \underset{˙}{\cdot} X) \underset{˙}{+} w)$
43		oveq2	$⊢ w = k \underset{˙}{\cdot} Y \to (j \underset{˙}{\cdot} X) \underset{˙}{+} w = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y)$
44	43	eqeq2d	$⊢ w = k \underset{˙}{\cdot} Y \to (U = (j \underset{˙}{\cdot} X) \underset{˙}{+} w \leftrightarrow U = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y))$
45	42 44	ceqsrex2v	$⊢ (j \underset{˙}{\cdot} X \in N (\{X\}) \land k \underset{˙}{\cdot} Y \in N (\{Y\})) \to (\exists v \in N (\{X\}) \exists w \in N (\{Y\}) ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow U = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y))$
46	37 40 45	syl2anc	$⊢ (φ \land (j \in K \land k \in K)) \to (\exists v \in N (\{X\}) \exists w \in N (\{Y\}) ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow U = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y))$
47	46	2rexbidva	$⊢ φ \to (\exists j \in K \exists k \in K \exists v \in N (\{X\}) \exists w \in N (\{Y\}) ((v = j \underset{˙}{\cdot} X \land w = k \underset{˙}{\cdot} Y) \land U = v \underset{˙}{+} w) \leftrightarrow \exists j \in K \exists k \in K U = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y))$
48	16 33 47	3bitrd	$⊢ φ \to (U \in (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \leftrightarrow \exists j \in K \exists k \in K U = (j \underset{˙}{\cdot} X) \underset{˙}{+} (k \underset{˙}{\cdot} Y))$

Metamath Proof Explorer

Theorem lsmspsn

Proof