Metamath Proof Explorer

Theorem pjclem1

Description: Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 ⊢G∈Cℋ
pjclem1.2 ⊢H∈Cℋ
Assertion pjclem1 ⊢G𝐶ℋH→projℎ⁡G∘projℎ⁡H=projℎ⁡G∩H

Proof

Step Hyp Ref Expression
1 pjclem1.1 ⊢G∈Cℋ
2 pjclem1.2 ⊢H∈Cℋ
3 1 2 cmbri ⊢G𝐶ℋH↔G=G∩H∨ℋG∩⊥⁡H
4 fveq2 ⊢G=G∩H∨ℋG∩⊥⁡H→projℎ⁡G=projℎ⁡G∩H∨ℋG∩⊥⁡H
5 3 4 sylbi ⊢G𝐶ℋH→projℎ⁡G=projℎ⁡G∩H∨ℋG∩⊥⁡H
6 inss2 ⊢G∩H⊆H
7 1 choccli ⊢⊥⁡G∈Cℋ
8 2 7 chub2i ⊢H⊆⊥⁡G∨ℋH
9 1 2 chdmm3i ⊢⊥⁡G∩⊥⁡H=⊥⁡G∨ℋH
10 8 9 sseqtrri ⊢H⊆⊥⁡G∩⊥⁡H
11 6 10 sstri ⊢G∩H⊆⊥⁡G∩⊥⁡H
12 1 2 chincli ⊢G∩H∈Cℋ
13 2 choccli ⊢⊥⁡H∈Cℋ
14 1 13 chincli ⊢G∩⊥⁡H∈Cℋ
15 12 14 pjscji ⊢G∩H⊆⊥⁡G∩⊥⁡H→projℎ⁡G∩H∨ℋG∩⊥⁡H=projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H
16 11 15 ax-mp ⊢projℎ⁡G∩H∨ℋG∩⊥⁡H=projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H
17 16 eqeq2i ⊢projℎ⁡G=projℎ⁡G∩H∨ℋG∩⊥⁡H↔projℎ⁡G=projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H
18 coeq2 ⊢projℎ⁡G=projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H→projℎ⁡H∘projℎ⁡G=projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H
19 12 pjfi ⊢projℎ⁡G∩H:ℋ⟶ℋ
20 14 pjfi ⊢projℎ⁡G∩⊥⁡H:ℋ⟶ℋ
21 2 19 20 pjsdii ⊢projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H=projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡H∘projℎ⁡G∩⊥⁡H
22 12 2 pjss1coi ⊢G∩H⊆H↔projℎ⁡H∘projℎ⁡G∩H=projℎ⁡G∩H
23 6 22 mpbi ⊢projℎ⁡H∘projℎ⁡G∩H=projℎ⁡G∩H
24 2 14 pjorthcoi ⊢H⊆⊥⁡G∩⊥⁡H→projℎ⁡H∘projℎ⁡G∩⊥⁡H=0hop
25 10 24 ax-mp ⊢projℎ⁡H∘projℎ⁡G∩⊥⁡H=0hop
26 23 25 oveq12i ⊢projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡H∘projℎ⁡G∩⊥⁡H=projℎ⁡G∩H+op0hop
27 19 hoaddridi ⊢projℎ⁡G∩H+op0hop=projℎ⁡G∩H
28 21 26 27 3eqtri ⊢projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H=projℎ⁡G∩H
29 28 eqeq2i ⊢projℎ⁡H∘projℎ⁡G=projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H↔projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H
30 coeq2 ⊢projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H→projℎ⁡G∘projℎ⁡H∘projℎ⁡G=projℎ⁡G∘projℎ⁡G∩H
31 inss1 ⊢G∩H⊆G
32 12 1 pjss1coi ⊢G∩H⊆G↔projℎ⁡G∘projℎ⁡G∩H=projℎ⁡G∩H
33 31 32 mpbi ⊢projℎ⁡G∘projℎ⁡G∩H=projℎ⁡G∩H
34 30 33 eqtrdi ⊢projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H→projℎ⁡G∘projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H
35 29 34 sylbi ⊢projℎ⁡H∘projℎ⁡G=projℎ⁡H∘projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H
36 18 35 syl ⊢projℎ⁡G=projℎ⁡G∩H+opprojℎ⁡G∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H
37 17 36 sylbi ⊢projℎ⁡G=projℎ⁡G∩H∨ℋG∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H
38 5 37 syl ⊢G𝐶ℋH→projℎ⁡G∘projℎ⁡H∘projℎ⁡G=projℎ⁡G∩H
39 1 2 cmcm3i ⊢G𝐶ℋH↔⊥⁡G𝐶ℋH
40 7 2 cmbri ⊢⊥⁡G𝐶ℋH↔⊥⁡G=⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H
41 39 40 bitri ⊢G𝐶ℋH↔⊥⁡G=⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H
42 fveq2 ⊢⊥⁡G=⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H→projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H
43 inss2 ⊢⊥⁡G∩H⊆H
44 2 1 chub2i ⊢H⊆G∨ℋH
45 1 2 chdmm4i ⊢⊥⁡⊥⁡G∩⊥⁡H=G∨ℋH
46 44 45 sseqtrri ⊢H⊆⊥⁡⊥⁡G∩⊥⁡H
47 43 46 sstri ⊢⊥⁡G∩H⊆⊥⁡⊥⁡G∩⊥⁡H
48 7 2 chincli ⊢⊥⁡G∩H∈Cℋ
49 7 13 chincli ⊢⊥⁡G∩⊥⁡H∈Cℋ
50 48 49 pjscji ⊢⊥⁡G∩H⊆⊥⁡⊥⁡G∩⊥⁡H→projℎ⁡⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H=projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H
51 47 50 ax-mp ⊢projℎ⁡⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H=projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H
52 51 eqeq2i ⊢projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H↔projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H
53 coeq2 ⊢projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H→projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H
54 48 pjfi ⊢projℎ⁡⊥⁡G∩H:ℋ⟶ℋ
55 49 pjfi ⊢projℎ⁡⊥⁡G∩⊥⁡H:ℋ⟶ℋ
56 2 54 55 pjsdii ⊢projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H=projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡H∘projℎ⁡⊥⁡G∩⊥⁡H
57 48 2 pjss1coi ⊢⊥⁡G∩H⊆H↔projℎ⁡H∘projℎ⁡⊥⁡G∩H=projℎ⁡⊥⁡G∩H
58 43 57 mpbi ⊢projℎ⁡H∘projℎ⁡⊥⁡G∩H=projℎ⁡⊥⁡G∩H
59 2 49 pjorthcoi ⊢H⊆⊥⁡⊥⁡G∩⊥⁡H→projℎ⁡H∘projℎ⁡⊥⁡G∩⊥⁡H=0hop
60 46 59 ax-mp ⊢projℎ⁡H∘projℎ⁡⊥⁡G∩⊥⁡H=0hop
61 58 60 oveq12i ⊢projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡H∘projℎ⁡⊥⁡G∩⊥⁡H=projℎ⁡⊥⁡G∩H+op0hop
62 54 hoaddridi ⊢projℎ⁡⊥⁡G∩H+op0hop=projℎ⁡⊥⁡G∩H
63 56 61 62 3eqtri ⊢projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H=projℎ⁡⊥⁡G∩H
64 63 eqeq2i ⊢projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H↔projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H
65 coeq2 ⊢projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡G∘projℎ⁡⊥⁡G∩H
66 1 13 chub1i ⊢G⊆G∨ℋ⊥⁡H
67 1 2 chdmm2i ⊢⊥⁡⊥⁡G∩H=G∨ℋ⊥⁡H
68 66 67 sseqtrri ⊢G⊆⊥⁡⊥⁡G∩H
69 1 48 pjorthcoi ⊢G⊆⊥⁡⊥⁡G∩H→projℎ⁡G∘projℎ⁡⊥⁡G∩H=0hop
70 68 69 ax-mp ⊢projℎ⁡G∘projℎ⁡⊥⁡G∩H=0hop
71 65 70 eqtrdi ⊢projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=0hop
72 64 71 sylbi ⊢projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡H∘projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=0hop
73 53 72 syl ⊢projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H+opprojℎ⁡⊥⁡G∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=0hop
74 52 73 sylbi ⊢projℎ⁡⊥⁡G=projℎ⁡⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=0hop
75 42 74 syl ⊢⊥⁡G=⊥⁡G∩H∨ℋ⊥⁡G∩⊥⁡H→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=0hop
76 41 75 sylbi ⊢G𝐶ℋH→projℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=0hop
77 38 76 oveq12d ⊢G𝐶ℋH→projℎ⁡G∘projℎ⁡H∘projℎ⁡G+opprojℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡G∩H+op0hop
78 df-iop ⊢Iop=projℎ⁡ℋ
79 78 coeq2i ⊢projℎ⁡H∘Iop=projℎ⁡H∘projℎ⁡ℋ
80 2 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
81 80 hoid1i ⊢projℎ⁡H∘Iop=projℎ⁡H
82 79 81 eqtr3i ⊢projℎ⁡H∘projℎ⁡ℋ=projℎ⁡H
83 1 pjtoi ⊢projℎ⁡G+opprojℎ⁡⊥⁡G=projℎ⁡ℋ
84 83 coeq2i ⊢projℎ⁡H∘projℎ⁡G+opprojℎ⁡⊥⁡G=projℎ⁡H∘projℎ⁡ℋ
85 1 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
86 7 pjfi ⊢projℎ⁡⊥⁡G:ℋ⟶ℋ
87 2 85 86 pjsdii ⊢projℎ⁡H∘projℎ⁡G+opprojℎ⁡⊥⁡G=projℎ⁡H∘projℎ⁡G+opprojℎ⁡H∘projℎ⁡⊥⁡G
88 84 87 eqtr3i ⊢projℎ⁡H∘projℎ⁡ℋ=projℎ⁡H∘projℎ⁡G+opprojℎ⁡H∘projℎ⁡⊥⁡G
89 82 88 eqtr3i ⊢projℎ⁡H=projℎ⁡H∘projℎ⁡G+opprojℎ⁡H∘projℎ⁡⊥⁡G
90 89 coeq2i ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G∘projℎ⁡H∘projℎ⁡G+opprojℎ⁡H∘projℎ⁡⊥⁡G
91 80 85 hocofi ⊢projℎ⁡H∘projℎ⁡G:ℋ⟶ℋ
92 80 86 hocofi ⊢projℎ⁡H∘projℎ⁡⊥⁡G:ℋ⟶ℋ
93 1 91 92 pjsdii ⊢projℎ⁡G∘projℎ⁡H∘projℎ⁡G+opprojℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡G∘projℎ⁡H∘projℎ⁡G+opprojℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G
94 90 93 eqtr2i ⊢projℎ⁡G∘projℎ⁡H∘projℎ⁡G+opprojℎ⁡G∘projℎ⁡H∘projℎ⁡⊥⁡G=projℎ⁡G∘projℎ⁡H
95 77 94 27 3eqtr3g ⊢G𝐶ℋH→projℎ⁡G∘projℎ⁡H=projℎ⁡G∩H