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

Metamath Proof Explorer

Theorem paddssw2

Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)

Ref Expression
Hypotheses paddssw.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddssw.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddssw2 ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 paddssw.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 paddssw.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 1 2 sspadd1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
4 3 3adant3r3 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
5 sstr ⊢ ( ( 𝑋 ⊆ ( 𝑋 + 𝑌 ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑋 ⊆ 𝑍 )
6 4 5 sylan ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑋 ⊆ 𝑍 )
7 6 ex ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → 𝑋 ⊆ 𝑍 ) )
8 simpl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝐾 ∈ 𝐵 )
9 simpr2 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑌 ⊆ 𝐴 )
10 simpr1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ 𝐴 )
11 1 2 sspadd2 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → 𝑌 ⊆ ( 𝑋 + 𝑌 ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑌 ⊆ ( 𝑋 + 𝑌 ) )
13 sstr ⊢ ( ( 𝑌 ⊆ ( 𝑋 + 𝑌 ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑌 ⊆ 𝑍 )
14 12 13 sylan ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) ∧ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) → 𝑌 ⊆ 𝑍 )
15 14 ex ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → 𝑌 ⊆ 𝑍 ) )
16 7 15 jcad ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )