Metamath Proof Explorer

Theorem pjsslem

Description: Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢H∈Cℋ
pjidm.2 ⊢A∈ℋ
pjsslem.1 ⊢G∈Cℋ
Assertion pjsslem ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A=projℎ⁡G⁡A-ℎprojℎ⁡H⁡A

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢H∈Cℋ
2 pjidm.2 ⊢A∈ℋ
3 pjsslem.1 ⊢G∈Cℋ
4 pjo ⊢H∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A
5 1 2 4 mp2an ⊢projℎ⁡⊥⁡H⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A
6 pjo ⊢G∈Cℋ∧A∈ℋ→projℎ⁡⊥⁡G⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡G⁡A
7 3 2 6 mp2an ⊢projℎ⁡⊥⁡G⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡G⁡A
8 5 7 oveq12i ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A-ℎprojℎ⁡ℋ⁡A-ℎprojℎ⁡G⁡A
9 helch ⊢ℋ∈Cℋ
10 9 2 pjclii ⊢projℎ⁡ℋ⁡A∈ℋ
11 1 2 pjhclii ⊢projℎ⁡H⁡A∈ℋ
12 3 2 pjhclii ⊢projℎ⁡G⁡A∈ℋ
13 10 11 10 12 hvsubsub4i ⊢projℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A-ℎprojℎ⁡ℋ⁡A-ℎprojℎ⁡G⁡A=projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A
14 hvsubid ⊢projℎ⁡ℋ⁡A∈ℋ→projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A=0ℎ
15 10 14 ax-mp ⊢projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A=0ℎ
16 15 oveq1i ⊢projℎ⁡ℋ⁡A-ℎprojℎ⁡ℋ⁡A-ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A=0ℎ-ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A
17 8 13 16 3eqtri ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A=0ℎ-ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A
18 11 12 hvsubcli ⊢projℎ⁡H⁡A-ℎprojℎ⁡G⁡A∈ℋ
19 18 hv2negi ⊢0ℎ-ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A=-1⋅ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A
20 11 12 hvnegdii ⊢-1⋅ℎprojℎ⁡H⁡A-ℎprojℎ⁡G⁡A=projℎ⁡G⁡A-ℎprojℎ⁡H⁡A
21 17 19 20 3eqtri ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A=projℎ⁡G⁡A-ℎprojℎ⁡H⁡A