This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )