osumclN

Description: Closure of orthogonal sum. If X and Y are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osumcl.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	osumcl.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	osumcl.c	$⊢ C = PSubCl (K)$
Assertion	osumclN	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to X \underset{˙}{+} Y \in C$

Proof

Step	Hyp	Ref	Expression
1		osumcl.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
2		osumcl.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		osumcl.c	$⊢ C = PSubCl (K)$
4		simpl1	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to K \in HL$
5		simpl2	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to X \in C$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	6 3	psubclssatN	$⊢ (K \in HL \land X \in C) \to X \subseteq Atoms (K)$
8	4 5 7	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to X \subseteq Atoms (K)$
9		simpl3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \in C$
10	6 3	psubclssatN	$⊢ (K \in HL \land Y \in C) \to Y \subseteq Atoms (K)$
11	4 9 10	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq Atoms (K)$
12	6 1	paddssat	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
13	4 8 11 12	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
14		simpll1	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X = \emptyset) \to K \in HL$
15		oveq1	$⊢ X = \emptyset \to X \underset{˙}{+} Y = \emptyset \underset{˙}{+} Y$
16	6 1	padd02	$⊢ (K \in HL \land Y \subseteq Atoms (K)) \to \emptyset \underset{˙}{+} Y = Y$
17	4 11 16	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to \emptyset \underset{˙}{+} Y = Y$
18	15 17	sylan9eqr	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X = \emptyset) \to X \underset{˙}{+} Y = Y$
19		simpll3	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X = \emptyset) \to Y \in C$
20	18 19	eqeltrd	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X = \emptyset) \to X \underset{˙}{+} Y \in C$
21	2 3	psubcli2N	$⊢ (K \in HL \land X \underset{˙}{+} Y \in C) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = X \underset{˙}{+} Y$
22	14 20 21	syl2anc	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X = \emptyset) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = X \underset{˙}{+} Y$
23	1 2 3	osumcllem11N	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \underset{˙}{+} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
24	23	anassrs	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X \neq \emptyset) \to X \underset{˙}{+} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
25	24	eqcomd	$⊢ (((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \land X \neq \emptyset) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = X \underset{˙}{+} Y$
26	22 25	pm2.61dane	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = X \underset{˙}{+} Y$
27	6 2 3	ispsubclN	$⊢ K \in HL \to (X \underset{˙}{+} Y \in C \leftrightarrow (X \underset{˙}{+} Y \subseteq Atoms (K) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = X \underset{˙}{+} Y))$
28	4 27	syl	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to (X \underset{˙}{+} Y \in C \leftrightarrow (X \underset{˙}{+} Y \subseteq Atoms (K) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = X \underset{˙}{+} Y))$
29	13 26 28	mpbir2and	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq \underset{˙}{⊥} (Y)) \to X \underset{˙}{+} Y \in C$

Metamath Proof Explorer

Theorem osumclN

Proof