Metamath Proof Explorer

Theorem paddss2

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

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

Proof

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