dvhopellsm

Description: Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014)

	Ref	Expression
Hypotheses	dvhopellsm.h	$⊢ H = LHyp (K)$
	dvhopellsm.u	$⊢ U = DVecH (K) (W)$
	dvhopellsm.a	$⊢ \underset{˙}{+} = +_{U}$
	dvhopellsm.s	$⊢ S = LSubSp (U)$
	dvhopellsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	dvhopellsm	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (⟨F, T⟩ \in (X \underset{˙}{\oplus} Y) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$

Proof

Step	Hyp	Ref	Expression
1		dvhopellsm.h	$⊢ H = LHyp (K)$
2		dvhopellsm.u	$⊢ U = DVecH (K) (W)$
3		dvhopellsm.a	$⊢ \underset{˙}{+} = +_{U}$
4		dvhopellsm.s	$⊢ S = LSubSp (U)$
5		dvhopellsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
6		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
7	1 2 6	dvhlmod	$⊢ (K \in HL \land W \in H) \to U \in LMod$
8	7	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to U \in LMod$
9	4	lsssssubg	$⊢ U \in LMod \to S \subseteq SubGrp (U)$
10	8 9	syl	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to S \subseteq SubGrp (U)$
11		simp2	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to X \in S$
12	10 11	sseldd	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to X \in SubGrp (U)$
13		simp3	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to Y \in S$
14	10 13	sseldd	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to Y \in SubGrp (U)$
15	3 5	lsmelval	$⊢ (X \in SubGrp (U) \land Y \in SubGrp (U)) \to (⟨F, T⟩ \in (X \underset{˙}{\oplus} Y) \leftrightarrow \exists u \in X \exists v \in Y ⟨F, T⟩ = u \underset{˙}{+} v)$
16	12 14 15	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (⟨F, T⟩ \in (X \underset{˙}{\oplus} Y) \leftrightarrow \exists u \in X \exists v \in Y ⟨F, T⟩ = u \underset{˙}{+} v)$
17		eqid	$⊢ {Base}_{U} = {Base}_{U}$
18	17 4	lssss	$⊢ Y \in S \to Y \subseteq {Base}_{U}$
19	18	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to Y \subseteq {Base}_{U}$
20		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
21		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
22	1 20 21 2 17	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = LTrn (K) (W) \times TEndo (K) (W)$
23	22	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to {Base}_{U} = LTrn (K) (W) \times TEndo (K) (W)$
24	19 23	sseqtrd	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to Y \subseteq LTrn (K) (W) \times TEndo (K) (W)$
25		relxp	$⊢ Rel (LTrn (K) (W) \times TEndo (K) (W))$
26		relss	$⊢ Y \subseteq LTrn (K) (W) \times TEndo (K) (W) \to (Rel (LTrn (K) (W) \times TEndo (K) (W)) \to Rel Y)$
27	24 25 26	mpisyl	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to Rel Y$
28		oveq2	$⊢ v = ⟨z, w⟩ \to u \underset{˙}{+} v = u \underset{˙}{+} ⟨z, w⟩$
29	28	eqeq2d	$⊢ v = ⟨z, w⟩ \to (⟨F, T⟩ = u \underset{˙}{+} v \leftrightarrow ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩)$
30	29	exopxfr2	$⊢ Rel Y \to (\exists v \in Y ⟨F, T⟩ = u \underset{˙}{+} v \leftrightarrow \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩))$
31	27 30	syl	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (\exists v \in Y ⟨F, T⟩ = u \underset{˙}{+} v \leftrightarrow \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩))$
32	31	rexbidv	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (\exists u \in X \exists v \in Y ⟨F, T⟩ = u \underset{˙}{+} v \leftrightarrow \exists u \in X \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩))$
33	17 4	lssss	$⊢ X \in S \to X \subseteq {Base}_{U}$
34	33	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to X \subseteq {Base}_{U}$
35	34 23	sseqtrd	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to X \subseteq LTrn (K) (W) \times TEndo (K) (W)$
36		relss	$⊢ X \subseteq LTrn (K) (W) \times TEndo (K) (W) \to (Rel (LTrn (K) (W) \times TEndo (K) (W)) \to Rel X)$
37	35 25 36	mpisyl	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to Rel X$
38		oveq1	$⊢ u = ⟨x, y⟩ \to u \underset{˙}{+} ⟨z, w⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩$
39	38	eqeq2d	$⊢ u = ⟨x, y⟩ \to (⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩ \leftrightarrow ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)$
40	39	anbi2d	$⊢ u = ⟨x, y⟩ \to ((⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩) \leftrightarrow (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
41	40	2exbidv	$⊢ u = ⟨x, y⟩ \to (\exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩) \leftrightarrow \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
42	41	exopxfr2	$⊢ Rel X \to (\exists u \in X \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩) \leftrightarrow \exists x \exists y (⟨x, y⟩ \in X \land \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)))$
43	37 42	syl	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (\exists u \in X \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩) \leftrightarrow \exists x \exists y (⟨x, y⟩ \in X \land \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)))$
44		19.42vv	$⊢ \exists z \exists w (⟨x, y⟩ \in X \land (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)) \leftrightarrow (⟨x, y⟩ \in X \land \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
45		anass	$⊢ ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow (⟨x, y⟩ \in X \land (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
46	45	2exbii	$⊢ \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow \exists z \exists w (⟨x, y⟩ \in X \land (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
47	46	bicomi	$⊢ \exists z \exists w (⟨x, y⟩ \in X \land (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)) \leftrightarrow \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)$
48	47	a1i	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (\exists z \exists w (⟨x, y⟩ \in X \land (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)) \leftrightarrow \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
49	44 48	syl5bbr	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to ((⟨x, y⟩ \in X \land \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)) \leftrightarrow \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
50	49	2exbidv	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (\exists x \exists y (⟨x, y⟩ \in X \land \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩)) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
51	43 50	bitrd	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (\exists u \in X \exists z \exists w (⟨z, w⟩ \in Y \land ⟨F, T⟩ = u \underset{˙}{+} ⟨z, w⟩) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
52	16 32 51	3bitrd	$⊢ ((K \in HL \land W \in H) \land X \in S \land Y \in S) \to (⟨F, T⟩ \in (X \underset{˙}{\oplus} Y) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in X \land ⟨z, w⟩ \in Y) \land ⟨F, T⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$

Metamath Proof Explorer

Theorem dvhopellsm

Proof