Metamath Proof Explorer

Theorem pjocini

Description: Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjocin.1 ⊢ G ∈ C ℋ
pjocin.2 ⊢ H ∈ C ℋ
Assertion pjocini ⊢ A ∈ ⊥ ⁡ G ∩ H → proj ℎ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H

Proof

Step Hyp Ref Expression
1 pjocin.1 ⊢ G ∈ C ℋ
2 pjocin.2 ⊢ H ∈ C ℋ
3 1 2 chincli ⊢ G ∩ H ∈ C ℋ
4 3 choccli ⊢ ⊥ ⁡ G ∩ H ∈ C ℋ
5 4 cheli ⊢ A ∈ ⊥ ⁡ G ∩ H → A ∈ ℋ
6 pjpo ⊢ G ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ G ⁡ A = A - ℎ proj ℎ ⁡ ⊥ ⁡ G ⁡ A
7 1 5 6 sylancr ⊢ A ∈ ⊥ ⁡ G ∩ H → proj ℎ ⁡ G ⁡ A = A - ℎ proj ℎ ⁡ ⊥ ⁡ G ⁡ A
8 inss1 ⊢ G ∩ H ⊆ G
9 3 1 chsscon3i ⊢ G ∩ H ⊆ G ↔ ⊥ ⁡ G ⊆ ⊥ ⁡ G ∩ H
10 8 9 mpbi ⊢ ⊥ ⁡ G ⊆ ⊥ ⁡ G ∩ H
11 1 choccli ⊢ ⊥ ⁡ G ∈ C ℋ
12 11 pjcli ⊢ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G
13 5 12 syl ⊢ A ∈ ⊥ ⁡ G ∩ H → proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G
14 10 13 sseldi ⊢ A ∈ ⊥ ⁡ G ∩ H → proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H
15 4 chshii ⊢ ⊥ ⁡ G ∩ H ∈ S ℋ
16 shsubcl ⊢ ⊥ ⁡ G ∩ H ∈ S ℋ ∧ A ∈ ⊥ ⁡ G ∩ H ∧ proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H → A - ℎ proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H
17 15 16 mp3an1 ⊢ A ∈ ⊥ ⁡ G ∩ H ∧ proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H → A - ℎ proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H
18 14 17 mpdan ⊢ A ∈ ⊥ ⁡ G ∩ H → A - ℎ proj ℎ ⁡ ⊥ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H
19 7 18 eqeltrd ⊢ A ∈ ⊥ ⁡ G ∩ H → proj ℎ ⁡ G ⁡ A ∈ ⊥ ⁡ G ∩ H