Metamath Proof Explorer

Theorem paddss1

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

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

Proof

Step Hyp Ref Expression
1 padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 ssel ⊢ ( 𝑋 ⊆ 𝑌 → ( 𝑝 ∈ 𝑋 → 𝑝 ∈ 𝑌 ) )
4 3 orim1d ⊢ ( 𝑋 ⊆ 𝑌 → ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍 ) → ( 𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍 ) ) )
5 ssrexv ⊢ ( 𝑋 ⊆ 𝑌 → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
6 5 anim2d ⊢ ( 𝑋 ⊆ 𝑌 → ( ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
7 4 6 orim12d ⊢ ( 𝑋 ⊆ 𝑌 → ( ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
8 7 adantl ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
9 simpl1 ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝐾 ∈ 𝐵 )
10 sstr ⊢ ( ( 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ 𝐴 )
11 10 3ad2antr2 ⊢ ( ( 𝑋 ⊆ 𝑌 ∧ ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ 𝐴 )
12 11 ancoms ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝐴 )
13 simpl3 ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑍 ⊆ 𝐴 )
14 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
16 14 15 1 2 elpadd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑝 ∈ ( 𝑋 + 𝑍 ) ↔ ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
17 9 12 13 16 syl3anc ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → ( 𝑝 ∈ ( 𝑋 + 𝑍 ) ↔ ( ( 𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
18 14 15 1 2 elpadd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑝 ∈ ( 𝑌 + 𝑍 ) ↔ ( ( 𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
19 18 adantr ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → ( 𝑝 ∈ ( 𝑌 + 𝑍 ) ↔ ( ( 𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍 ) ∨ ( 𝑝 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑌 ∃ 𝑟 ∈ 𝑍 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
20 8 17 19 3imtr4d ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → ( 𝑝 ∈ ( 𝑋 + 𝑍 ) → 𝑝 ∈ ( 𝑌 + 𝑍 ) ) )
21 20 ssrdv ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑋 ⊆ 𝑌 ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑍 ) )
22 21 ex ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑋 ⊆ 𝑌 → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + 𝑍 ) ) )