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

Metamath Proof Explorer

Theorem paddss

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

Ref Expression
Hypotheses paddss.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddss.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
paddss.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddss ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ↔ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 paddss.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 paddss.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 paddss.p ⊢ + = ( +𝑃 ‘ 𝐾 )
4 simpl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝐾 ∈ 𝐵 )
5 simpr1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑋 ⊆ 𝐴 )
6 simpr2 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑌 ⊆ 𝐴 )
7 1 2 psubssat ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑍 ∈ 𝑆 ) → 𝑍 ⊆ 𝐴 )
8 7 3ad2antr3 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → 𝑍 ⊆ 𝐴 )
9 1 3 paddssw1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )
10 4 5 6 8 9 syl13anc ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ) )
11 2 3 paddidm ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑍 + 𝑍 ) = 𝑍 )
12 11 3ad2antr3 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( 𝑍 + 𝑍 ) = 𝑍 )
13 12 sseq2d ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ ( 𝑍 + 𝑍 ) ↔ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )
14 10 13 sylibd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) → ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )
15 1 3 paddssw2 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )
16 4 5 6 8 15 syl13anc ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) ⊆ 𝑍 → ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ) )
17 14 16 impbid ⊢ ( ( 𝐾 ∈ 𝐵 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆 ) ) → ( ( 𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍 ) ↔ ( 𝑋 + 𝑌 ) ⊆ 𝑍 ) )