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 𝐴 = ( Atoms ‘ 𝐾 )
paddatcl.p + = ( +𝑃𝐾 )
paddatcl.c 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion paddatclN ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( 𝑋 + { 𝑄 } ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 paddatcl.a 𝐴 = ( Atoms ‘ 𝐾 )
2 paddatcl.p + = ( +𝑃𝐾 )
3 paddatcl.c 𝐶 = ( PSubCl ‘ 𝐾 )
4 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
5 4 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → 𝐾 ∈ CLat )
6 1 3 psubclssatN ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → 𝑋𝐴 )
7 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 1 atssbase 𝐴 ⊆ ( Base ‘ 𝐾 )
9 6 8 sstrdi ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
10 9 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
11 eqid ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
12 7 11 clatlubcl ( ( 𝐾 ∈ CLat ∧ 𝑋 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
13 5 10 12 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
14 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
15 eqid ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
16 7 14 1 15 2 pmapjat1 ( ( 𝐾 ∈ HL ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) + ( ( pmap ‘ 𝐾 ) ‘ 𝑄 ) ) )
17 13 16 syld3an2 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) + ( ( pmap ‘ 𝐾 ) ‘ 𝑄 ) ) )
18 11 15 3 pmapidclN ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
19 18 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
20 1 15 pmapat ( ( 𝐾 ∈ HL ∧ 𝑄𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ 𝑄 ) = { 𝑄 } )
21 20 3adant2 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ 𝑄 ) = { 𝑄 } )
22 19 21 oveq12d ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) + ( ( pmap ‘ 𝐾 ) ‘ 𝑄 ) ) = ( 𝑋 + { 𝑄 } ) )
23 17 22 eqtr2d ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( 𝑋 + { 𝑄 } ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ) )
24 simp1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → 𝐾 ∈ HL )
25 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
26 25 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → 𝐾 ∈ Lat )
27 7 1 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
28 27 3ad2ant3 ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
29 7 14 latjcl ( ( 𝐾 ∈ Lat ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
30 26 13 28 29 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
31 7 15 3 pmapsubclN ( ( 𝐾 ∈ HL ∧ ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ) ∈ 𝐶 )
32 24 30 31 syl2anc ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑄 ) ) ∈ 𝐶 )
33 23 32 eqeltrd ( ( 𝐾 ∈ HL ∧ 𝑋𝐶𝑄𝐴 ) → ( 𝑋 + { 𝑄 } ) ∈ 𝐶 )