Metamath Proof Explorer

Theorem pclunN

Description: The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclun.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pclun.p ⊢ + = ( +𝑃 ‘ 𝐾 )
pclun.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion pclunN ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 pclun.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pclun.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 pclun.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
4 simp1 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝐾 ∈ 𝑉 )
5 1 2 paddunssN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑋 + 𝑌 ) )
6 1 2 paddssat ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
7 1 3 pclssN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑋 + 𝑌 ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) )
8 4 5 6 7 syl3anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) )
9 unss ⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ↔ ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 )
10 9 biimpi ⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 )
11 10 3adant1 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 )
12 1 3 pclssidN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
13 4 11 12 syl2anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
14 unss ⊢ ( ( 𝑋 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∧ 𝑌 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) ↔ ( 𝑋 ∪ 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
15 13 14 sylibr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∧ 𝑌 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
16 simp2 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ 𝐴 )
17 simp3 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑌 ⊆ 𝐴 )
18 eqid ⊢ ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
19 1 18 3 pclclN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑋 ∪ 𝑌 ) ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∈ ( PSubSp ‘ 𝐾 ) )
20 4 11 19 syl2anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∈ ( PSubSp ‘ 𝐾 ) )
21 1 18 2 paddss ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∈ ( PSubSp ‘ 𝐾 ) ) ) → ( ( 𝑋 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∧ 𝑌 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) ↔ ( 𝑋 + 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
22 4 16 17 20 21 syl13anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∧ 𝑌 ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) ↔ ( 𝑋 + 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
23 15 22 mpbid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
24 1 18 psubssat ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∈ ( PSubSp ‘ 𝐾 ) ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ 𝐴 )
25 4 20 24 syl2anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ 𝐴 )
26 1 3 pclssN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑋 + 𝑌 ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∧ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) ⊆ ( 𝑈 ‘ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
27 4 23 25 26 syl3anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) ⊆ ( 𝑈 ‘ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
28 18 3 pclidN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ∈ ( PSubSp ‘ 𝐾 ) ) → ( 𝑈 ‘ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) = ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
29 4 20 28 syl2anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) ) = ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
30 27 29 sseqtrd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) ⊆ ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) )
31 8 30 eqssd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) )