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

Metamath Proof Explorer

Theorem padd02

Description: Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion padd02 ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( ∅ + 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 simpl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → 𝐾 ∈ 𝐵 )
4 0ss ⊢ ∅ ⊆ 𝐴
5 4 a1i ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ∅ ⊆ 𝐴 )
6 simpr ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ 𝐴 )
7 3 5 6 3jca ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐾 ∈ 𝐵 ∧ ∅ ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) )
8 neirr ⊢ ¬ ∅ ≠ ∅
9 8 intnanr ⊢ ¬ ( ∅ ≠ ∅ ∧ 𝑋 ≠ ∅ )
10 1 2 paddval0 ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ ∅ ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) ∧ ¬ ( ∅ ≠ ∅ ∧ 𝑋 ≠ ∅ ) ) → ( ∅ + 𝑋 ) = ( ∅ ∪ 𝑋 ) )
11 7 9 10 sylancl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( ∅ + 𝑋 ) = ( ∅ ∪ 𝑋 ) )
12 uncom ⊢ ( ∅ ∪ 𝑋 ) = ( 𝑋 ∪ ∅ )
13 un0 ⊢ ( 𝑋 ∪ ∅ ) = 𝑋
14 12 13 eqtri ⊢ ( ∅ ∪ 𝑋 ) = 𝑋
15 11 14 eqtrdi ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( ∅ + 𝑋 ) = 𝑋 )