Metamath Proof Explorer

Theorem pclun2N

Description: The projective subspace closure of the union of two subspaces equals their projective sum. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pclun2.s	$⊢ S = PSubSp (K)$
		pclun2.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
		pclun2.c	$⊢ U = PCl (K)$
	Assertion	pclun2N	$⊢ (K \in HL \land X \in S \land Y \in S) \to U (X \cup Y) = X \underset{˙}{+} Y$

Proof

Step	Hyp	Ref	Expression
1		pclun2.s	$⊢ S = PSubSp (K)$
2		pclun2.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		pclun2.c	$⊢ U = PCl (K)$
4		simp1	$⊢ (K \in HL \land X \in S \land Y \in S) \to K \in HL$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	5 1	psubssat	$⊢ (K \in HL \land X \in S) \to X \subseteq Atoms (K)$
7	6	3adant3	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \subseteq Atoms (K)$
8	5 1	psubssat	$⊢ (K \in HL \land Y \in S) \to Y \subseteq Atoms (K)$
9	8	3adant2	$⊢ (K \in HL \land X \in S \land Y \in S) \to Y \subseteq Atoms (K)$
10	5 2 3	pclunN	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \to U (X \cup Y) = U (X \underset{˙}{+} Y)$
11	4 7 9 10	syl3anc	$⊢ (K \in HL \land X \in S \land Y \in S) \to U (X \cup Y) = U (X \underset{˙}{+} Y)$
12	1 2	paddclN	$⊢ (K \in HL \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$
13	1 3	pclidN	$⊢ (K \in HL \land X \underset{˙}{+} Y \in S) \to U (X \underset{˙}{+} Y) = X \underset{˙}{+} Y$
14	4 12 13	syl2anc	$⊢ (K \in HL \land X \in S \land Y \in S) \to U (X \underset{˙}{+} Y) = X \underset{˙}{+} Y$
15	11 14	eqtrd	$⊢ (K \in HL \land X \in S \land Y \in S) \to U (X \cup Y) = X \underset{˙}{+} Y$