lrelat

Description: Subspaces are relatively atomic. Remark 2 of Kalmbach p. 149. ( chrelati analog.) (Contributed by NM, 11-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lrelat.s	$⊢ S = LSubSp (W)$
2		lrelat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lrelat.a	$⊢ A = LSAtoms (W)$
4		lrelat.w	$⊢ φ \to W \in LMod$
5		lrelat.t	$⊢ φ \to T \in S$
6		lrelat.u	$⊢ φ \to U \in S$
7		lrelat.l	$⊢ φ \to T \subset U$
8	1 3 4 5 6 7	lpssat	$⊢ φ \to \exists q \in A (q \subseteq U \land \neg q \subseteq T)$
9		ancom	$⊢ (q \subseteq U \land \neg q \subseteq T) \leftrightarrow (\neg q \subseteq T \land q \subseteq U)$
10	4	adantr	$⊢ (φ \land q \in A) \to W \in LMod$
11	1	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
12	10 11	syl	$⊢ (φ \land q \in A) \to S \subseteq SubGrp (W)$
13	5	adantr	$⊢ (φ \land q \in A) \to T \in S$
14	12 13	sseldd	$⊢ (φ \land q \in A) \to T \in SubGrp (W)$
15		simpr	$⊢ (φ \land q \in A) \to q \in A$
16	1 3 10 15	lsatlssel	$⊢ (φ \land q \in A) \to q \in S$
17	12 16	sseldd	$⊢ (φ \land q \in A) \to q \in SubGrp (W)$
18	2 14 17	lssnle	$⊢ (φ \land q \in A) \to (\neg q \subseteq T \leftrightarrow T \subset T \underset{˙}{\oplus} q)$
19	7	pssssd	$⊢ φ \to T \subseteq U$
20	19	adantr	$⊢ (φ \land q \in A) \to T \subseteq U$
21	20	biantrurd	$⊢ (φ \land q \in A) \to (q \subseteq U \leftrightarrow (T \subseteq U \land q \subseteq U))$
22	6	adantr	$⊢ (φ \land q \in A) \to U \in S$
23	12 22	sseldd	$⊢ (φ \land q \in A) \to U \in SubGrp (W)$
24	2	lsmlub	$⊢ (T \in SubGrp (W) \land q \in SubGrp (W) \land U \in SubGrp (W)) \to ((T \subseteq U \land q \subseteq U) \leftrightarrow T \underset{˙}{\oplus} q \subseteq U)$
25	14 17 23 24	syl3anc	$⊢ (φ \land q \in A) \to ((T \subseteq U \land q \subseteq U) \leftrightarrow T \underset{˙}{\oplus} q \subseteq U)$
26	21 25	bitrd	$⊢ (φ \land q \in A) \to (q \subseteq U \leftrightarrow T \underset{˙}{\oplus} q \subseteq U)$
27	18 26	anbi12d	$⊢ (φ \land q \in A) \to ((\neg q \subseteq T \land q \subseteq U) \leftrightarrow (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U))$
28	9 27	bitrid	$⊢ (φ \land q \in A) \to ((q \subseteq U \land \neg q \subseteq T) \leftrightarrow (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U))$
29	28	rexbidva	$⊢ φ \to (\exists q \in A (q \subseteq U \land \neg q \subseteq T) \leftrightarrow \exists q \in A (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U))$
30	8 29	mpbid	$⊢ φ \to \exists q \in A (T \subset T \underset{˙}{\oplus} q \land T \underset{˙}{\oplus} q \subseteq U)$

Metamath Proof Explorer

Theorem lrelat

Proof