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

Metamath Proof Explorer

Theorem pclun2N

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

Ref Expression
Hypotheses pclun2.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pclun2.p ⊢ + = ( +𝑃 ‘ 𝐾 )
pclun2.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion pclun2N ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( 𝑋 + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pclun2.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2 pclun2.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 pclun2.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
4 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝐾 ∈ HL )
5 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 5 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
7 6 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
8 5 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
9 8 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
10 5 2 3 pclunN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) )
11 4 7 9 10 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) )
12 1 2 paddclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
13 1 3 pclidN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ∈ 𝑆 ) → ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
14 4 12 13 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑈 ‘ ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
15 11 14 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑈 ‘ ( 𝑋 ∪ 𝑌 ) ) = ( 𝑋 + 𝑌 ) )