Metamath Proof Explorer

Theorem lcvexch

Description: Subspaces satisfy the exchange axiom. Lemma 7.5 of MaedaMaeda p. 31. ( cvexchi analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015)

		Ref	Expression
	Hypotheses	lcvexch.s	$⊢ S = LSubSp (W)$
		lcvexch.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
		lcvexch.c	$⊢ C = ⋖_{L} (W)$
		lcvexch.w	$⊢ φ \to W \in LMod$
		lcvexch.t	$⊢ φ \to T \in S$
		lcvexch.u	$⊢ φ \to U \in S$
	Assertion	lcvexch	$⊢ φ \to ((T \cap U) C U \leftrightarrow T C (T \underset{˙}{\oplus} U))$

Proof

Step	Hyp	Ref	Expression
1		lcvexch.s	$⊢ S = LSubSp (W)$
2		lcvexch.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lcvexch.c	$⊢ C = ⋖_{L} (W)$
4		lcvexch.w	$⊢ φ \to W \in LMod$
5		lcvexch.t	$⊢ φ \to T \in S$
6		lcvexch.u	$⊢ φ \to U \in S$
7	4	adantr	$⊢ (φ \land (T \cap U) C U) \to W \in LMod$
8	5	adantr	$⊢ (φ \land (T \cap U) C U) \to T \in S$
9	6	adantr	$⊢ (φ \land (T \cap U) C U) \to U \in S$
10		simpr	$⊢ (φ \land (T \cap U) C U) \to (T \cap U) C U$
11	1 2 3 7 8 9 10	lcvexchlem5	$⊢ (φ \land (T \cap U) C U) \to T C (T \underset{˙}{\oplus} U)$
12	4	adantr	$⊢ (φ \land T C (T \underset{˙}{\oplus} U)) \to W \in LMod$
13	5	adantr	$⊢ (φ \land T C (T \underset{˙}{\oplus} U)) \to T \in S$
14	6	adantr	$⊢ (φ \land T C (T \underset{˙}{\oplus} U)) \to U \in S$
15		simpr	$⊢ (φ \land T C (T \underset{˙}{\oplus} U)) \to T C (T \underset{˙}{\oplus} U)$
16	1 2 3 12 13 14 15	lcvexchlem4	$⊢ (φ \land T C (T \underset{˙}{\oplus} U)) \to (T \cap U) C U$
17	11 16	impbida	$⊢ φ \to ((T \cap U) C U \leftrightarrow T C (T \underset{˙}{\oplus} U))$