Theorem 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	|- .+ = ( +P ` K )
	paddatcl.c	|- C = ( PSubCl ` K )
Assertion	paddatclN	|- ( ( K e. HL /\ X e. C /\ Q e. A ) -> ( X .+ { Q } ) e. C )

Proof

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