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

Metamath Proof Explorer

Theorem paddss12

Description: Subset law for projective subspace sum. ( unss12 analog.) (Contributed by NM, 7-Mar-2012)

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

Proof

Step Hyp Ref Expression
1 padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 simpl1 ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝐾 ∈ 𝐵 )
4 simpl2 ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑌 ⊆ 𝐴 )
5 sstr ⊢ ( ( 𝑍 ⊆ 𝑊 ∧ 𝑊 ⊆ 𝐴 ) → 𝑍 ⊆ 𝐴 )
6 5 ancoms ⊢ ( ( 𝑊 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝑊 ) → 𝑍 ⊆ 𝐴 )
7 6 ad2ant2l ⊢ ( ( ( 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑍 ⊆ 𝐴 )
8 7 3adantl1 ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑍 ⊆ 𝐴 )
9 3 4 8 3jca ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) )
10 simprl ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → 𝑋 ⊆ 𝑌 )
11 1 2 paddss1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑋 ⊆ 𝑌 → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑍 ) ) )
12 9 10 11 sylc ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑍 ) )
13 1 2 paddss2 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑍 ⊆ 𝑊 → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) ) )
14 13 3com23 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) → ( 𝑍 ⊆ 𝑊 → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) ) )
15 14 imp ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑊 ) → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) )
16 15 adantrl ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝑌 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) )
17 12 16 sstrd ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) )
18 17 ex ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊 ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑊 ) ) )