paddclN

Description: The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of MaedaMaeda p. 68. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	paddidm.s	$⊢ S = PSubSp (K)$
	paddidm.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	paddclN	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$

Proof

Step	Hyp	Ref	Expression
1		paddidm.s	$⊢ S = PSubSp (K)$
2		paddidm.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		simp1	$⊢ (K \in HL \land X \in S \land Y \in S) \to K \in HL$
4		eqid	$⊢ Atoms (K) = Atoms (K)$
5	4 1	psubssat	$⊢ (K \in HL \land X \in S) \to X \subseteq Atoms (K)$
6	5	3adant3	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \subseteq Atoms (K)$
7	4 1	psubssat	$⊢ (K \in HL \land Y \in S) \to Y \subseteq Atoms (K)$
8	7	3adant2	$⊢ (K \in HL \land X \in S \land Y \in S) \to Y \subseteq Atoms (K)$
9	4 2	paddssat	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
10	3 6 8 9	syl3anc	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
11		olc	$⊢ (p \in Atoms (K) \land \exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r)) \to ((p \in (X \underset{˙}{+} Y) \lor p \in (X \underset{˙}{+} Y)) \lor (p \in Atoms (K) \land \exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r)))$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13		eqid	$⊢ join (K) = join (K)$
14	12 13 4 2	elpadd	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq Atoms (K) \land X \underset{˙}{+} Y \subseteq Atoms (K)) \to (p \in ((X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)) \leftrightarrow ((p \in (X \underset{˙}{+} Y) \lor p \in (X \underset{˙}{+} Y)) \lor (p \in Atoms (K) \land \exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r))))$
15	3 10 10 14	syl3anc	$⊢ (K \in HL \land X \in S \land Y \in S) \to (p \in ((X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)) \leftrightarrow ((p \in (X \underset{˙}{+} Y) \lor p \in (X \underset{˙}{+} Y)) \lor (p \in Atoms (K) \land \exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r))))$
16	4 2	padd4N	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \land (X \subseteq Atoms (K) \land Y \subseteq Atoms (K))) \to (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y) = (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y)$
17	3 6 8 6 8 16	syl122anc	$⊢ (K \in HL \land X \in S \land Y \in S) \to (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y) = (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y)$
18	1 2	paddidm	$⊢ (K \in HL \land X \in S) \to X \underset{˙}{+} X = X$
19	18	3adant3	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \underset{˙}{+} X = X$
20	1 2	paddidm	$⊢ (K \in HL \land Y \in S) \to Y \underset{˙}{+} Y = Y$
21	20	3adant2	$⊢ (K \in HL \land X \in S \land Y \in S) \to Y \underset{˙}{+} Y = Y$
22	19 21	oveq12d	$⊢ (K \in HL \land X \in S \land Y \in S) \to (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y) = X \underset{˙}{+} Y$
23	17 22	eqtrd	$⊢ (K \in HL \land X \in S \land Y \in S) \to (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y) = X \underset{˙}{+} Y$
24	23	eleq2d	$⊢ (K \in HL \land X \in S \land Y \in S) \to (p \in ((X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)) \leftrightarrow p \in (X \underset{˙}{+} Y))$
25	15 24	bitr3d	$⊢ (K \in HL \land X \in S \land Y \in S) \to (((p \in (X \underset{˙}{+} Y) \lor p \in (X \underset{˙}{+} Y)) \lor (p \in Atoms (K) \land \exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r))) \leftrightarrow p \in (X \underset{˙}{+} Y))$
26	11 25	imbitrid	$⊢ (K \in HL \land X \in S \land Y \in S) \to ((p \in Atoms (K) \land \exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r)) \to p \in (X \underset{˙}{+} Y))$
27	26	expd	$⊢ (K \in HL \land X \in S \land Y \in S) \to (p \in Atoms (K) \to (\exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r) \to p \in (X \underset{˙}{+} Y)))$
28	27	ralrimiv	$⊢ (K \in HL \land X \in S \land Y \in S) \to \forall p \in Atoms (K) (\exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r) \to p \in (X \underset{˙}{+} Y))$
29	12 13 4 1	ispsubsp2	$⊢ K \in HL \to (X \underset{˙}{+} Y \in S \leftrightarrow (X \underset{˙}{+} Y \subseteq Atoms (K) \land \forall p \in Atoms (K) (\exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r) \to p \in (X \underset{˙}{+} Y))))$
30	29	3ad2ant1	$⊢ (K \in HL \land X \in S \land Y \in S) \to (X \underset{˙}{+} Y \in S \leftrightarrow (X \underset{˙}{+} Y \subseteq Atoms (K) \land \forall p \in Atoms (K) (\exists q \in (X \underset{˙}{+} Y) \exists r \in (X \underset{˙}{+} Y) p \leq_{K} (q join (K) r) \to p \in (X \underset{˙}{+} Y))))$
31	10 28 30	mpbir2and	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$

Metamath Proof Explorer

Theorem paddclN

Proof