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 ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑋 + { 𝑄 } ) ∈ 𝐶 )