paddatclN

Description: The projective sum of a closed subspace and an atom is a closed projective subspace. (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	paddatcl.a	$⊢ A = Atoms (K)$
	paddatcl.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	paddatcl.c	$⊢ C = PSubCl (K)$
Assertion	paddatclN	$⊢ (K \in HL \land X \in C \land Q \in A) \to X \underset{˙}{+} \{Q\} \in C$

Proof

Step	Hyp	Ref	Expression
1		paddatcl.a	$⊢ A = Atoms (K)$
2		paddatcl.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		paddatcl.c	$⊢ C = PSubCl (K)$
4		hlclat	$⊢ K \in HL \to K \in CLat$
5	4	3ad2ant1	$⊢ (K \in HL \land X \in C \land Q \in A) \to K \in CLat$
6	1 3	psubclssatN	$⊢ (K \in HL \land X \in C) \to X \subseteq A$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 1	atssbase	$⊢ A \subseteq {Base}_{K}$
9	6 8	sstrdi	$⊢ (K \in HL \land X \in C) \to X \subseteq {Base}_{K}$
10	9	3adant3	$⊢ (K \in HL \land X \in C \land Q \in A) \to X \subseteq {Base}_{K}$
11		eqid	$⊢ lub (K) = lub (K)$
12	7 11	clatlubcl	$⊢ (K \in CLat \land X \subseteq {Base}_{K}) \to lub (K) (X) \in {Base}_{K}$
13	5 10 12	syl2anc	$⊢ (K \in HL \land X \in C \land Q \in A) \to lub (K) (X) \in {Base}_{K}$
14		eqid	$⊢ join (K) = join (K)$
15		eqid	$⊢ pmap (K) = pmap (K)$
16	7 14 1 15 2	pmapjat1	$⊢ (K \in HL \land lub (K) (X) \in {Base}_{K} \land Q \in A) \to pmap (K) (lub (K) (X) join (K) Q) = pmap (K) (lub (K) (X)) \underset{˙}{+} pmap (K) (Q)$
17	13 16	syld3an2	$⊢ (K \in HL \land X \in C \land Q \in A) \to pmap (K) (lub (K) (X) join (K) Q) = pmap (K) (lub (K) (X)) \underset{˙}{+} pmap (K) (Q)$
18	11 15 3	pmapidclN	$⊢ (K \in HL \land X \in C) \to pmap (K) (lub (K) (X)) = X$
19	18	3adant3	$⊢ (K \in HL \land X \in C \land Q \in A) \to pmap (K) (lub (K) (X)) = X$
20	1 15	pmapat	$⊢ (K \in HL \land Q \in A) \to pmap (K) (Q) = \{Q\}$
21	20	3adant2	$⊢ (K \in HL \land X \in C \land Q \in A) \to pmap (K) (Q) = \{Q\}$
22	19 21	oveq12d	$⊢ (K \in HL \land X \in C \land Q \in A) \to pmap (K) (lub (K) (X)) \underset{˙}{+} pmap (K) (Q) = X \underset{˙}{+} \{Q\}$
23	17 22	eqtr2d	$⊢ (K \in HL \land X \in C \land Q \in A) \to X \underset{˙}{+} \{Q\} = pmap (K) (lub (K) (X) join (K) Q)$
24		simp1	$⊢ (K \in HL \land X \in C \land Q \in A) \to K \in HL$
25		hllat	$⊢ K \in HL \to K \in Lat$
26	25	3ad2ant1	$⊢ (K \in HL \land X \in C \land Q \in A) \to K \in Lat$
27	7 1	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
28	27	3ad2ant3	$⊢ (K \in HL \land X \in C \land Q \in A) \to Q \in {Base}_{K}$
29	7 14	latjcl	$⊢ (K \in Lat \land lub (K) (X) \in {Base}_{K} \land Q \in {Base}_{K}) \to lub (K) (X) join (K) Q \in {Base}_{K}$
30	26 13 28 29	syl3anc	$⊢ (K \in HL \land X \in C \land Q \in A) \to lub (K) (X) join (K) Q \in {Base}_{K}$
31	7 15 3	pmapsubclN	$⊢ (K \in HL \land lub (K) (X) join (K) Q \in {Base}_{K}) \to pmap (K) (lub (K) (X) join (K) Q) \in C$
32	24 30 31	syl2anc	$⊢ (K \in HL \land X \in C \land Q \in A) \to pmap (K) (lub (K) (X) join (K) Q) \in C$
33	23 32	eqeltrd	$⊢ (K \in HL \land X \in C \land Q \in A) \to X \underset{˙}{+} \{Q\} \in C$

Metamath Proof Explorer

Theorem paddatclN

Proof