Metamath Proof Explorer

Theorem pjss2i

Description: Subset relationship for projections. Theorem 4.5(i)->(ii) of Beran p. 112. (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 pjss2i ⊢H⊆G→projℎ⁡H⁡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 1 choccli ⊢⊥⁡H∈Cℋ
5 4 2 pjclii ⊢projℎ⁡⊥⁡H⁡A∈⊥⁡H
6 1 3 chsscon3i ⊢H⊆G↔⊥⁡G⊆⊥⁡H
7 3 choccli ⊢⊥⁡G∈Cℋ
8 7 2 pjclii ⊢projℎ⁡⊥⁡G⁡A∈⊥⁡G
9 ssel ⊢⊥⁡G⊆⊥⁡H→projℎ⁡⊥⁡G⁡A∈⊥⁡G→projℎ⁡⊥⁡G⁡A∈⊥⁡H
10 8 9 mpi ⊢⊥⁡G⊆⊥⁡H→projℎ⁡⊥⁡G⁡A∈⊥⁡H
11 6 10 sylbi ⊢H⊆G→projℎ⁡⊥⁡G⁡A∈⊥⁡H
12 4 chshii ⊢⊥⁡H∈Sℋ
13 shsubcl ⊢⊥⁡H∈Sℋ∧projℎ⁡⊥⁡H⁡A∈⊥⁡H∧projℎ⁡⊥⁡G⁡A∈⊥⁡H→projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A∈⊥⁡H
14 12 13 mp3an1 ⊢projℎ⁡⊥⁡H⁡A∈⊥⁡H∧projℎ⁡⊥⁡G⁡A∈⊥⁡H→projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A∈⊥⁡H
15 5 11 14 sylancr ⊢H⊆G→projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A∈⊥⁡H
16 1 2 3 pjsslem ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A=projℎ⁡G⁡A-ℎprojℎ⁡H⁡A
17 16 eleq1i ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A∈⊥⁡H↔projℎ⁡G⁡A-ℎprojℎ⁡H⁡A∈⊥⁡H
18 3 2 pjhclii ⊢projℎ⁡G⁡A∈ℋ
19 1 2 pjhclii ⊢projℎ⁡H⁡A∈ℋ
20 18 19 hvsubcli ⊢projℎ⁡G⁡A-ℎprojℎ⁡H⁡A∈ℋ
21 1 20 pjoc2i ⊢projℎ⁡G⁡A-ℎprojℎ⁡H⁡A∈⊥⁡H↔projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡A=0ℎ
22 17 21 bitri ⊢projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A∈⊥⁡H↔projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡A=0ℎ
23 1 18 19 pjsubii ⊢projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡A=projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡projℎ⁡H⁡A
24 23 eqeq1i ⊢projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡A=0ℎ↔projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡projℎ⁡H⁡A=0ℎ
25 1 18 pjhclii ⊢projℎ⁡H⁡projℎ⁡G⁡A∈ℋ
26 1 19 pjhclii ⊢projℎ⁡H⁡projℎ⁡H⁡A∈ℋ
27 25 26 hvsubeq0i ⊢projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡projℎ⁡H⁡A=0ℎ↔projℎ⁡H⁡projℎ⁡G⁡A=projℎ⁡H⁡projℎ⁡H⁡A
28 24 27 bitri ⊢projℎ⁡H⁡projℎ⁡G⁡A-ℎprojℎ⁡H⁡A=0ℎ↔projℎ⁡H⁡projℎ⁡G⁡A=projℎ⁡H⁡projℎ⁡H⁡A
29 1 2 pjidmi ⊢projℎ⁡H⁡projℎ⁡H⁡A=projℎ⁡H⁡A
30 29 eqeq2i ⊢projℎ⁡H⁡projℎ⁡G⁡A=projℎ⁡H⁡projℎ⁡H⁡A↔projℎ⁡H⁡projℎ⁡G⁡A=projℎ⁡H⁡A
31 22 28 30 3bitrri ⊢projℎ⁡H⁡projℎ⁡G⁡A=projℎ⁡H⁡A↔projℎ⁡⊥⁡H⁡A-ℎprojℎ⁡⊥⁡G⁡A∈⊥⁡H
32 15 31 sylibr ⊢H⊆G→projℎ⁡H⁡projℎ⁡G⁡A=projℎ⁡H⁡A