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 + op proj G H
16 11 15 ax-mp proj G H G H = proj G H + op proj G H
17 16 eqeq2i proj G = proj G H G H proj G = proj G H + op proj G H
18 coeq2 proj G = proj G H + op proj G H proj H proj G = proj H proj G H + op proj G H
19 12 pjfi proj G H :
20 14 pjfi proj G H :
21 2 19 20 pjsdii proj H proj G H + op proj G H = proj H proj G H + op proj 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 = 0 hop
25 10 24 ax-mp proj H proj G H = 0 hop
26 23 25 oveq12i proj H proj G H + op proj H proj G H = proj G H + op 0 hop
27 19 hoaddid1i proj G H + op 0 hop = proj G H
28 21 26 27 3eqtri proj H proj G H + op proj G H = proj G H
29 28 eqeq2i proj H proj G = proj H proj G H + op proj 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 syl6eq 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 + op proj G H proj G proj H proj G = proj G H
36 18 35 syl proj G = proj G H + op proj 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 + op proj G H
51 47 50 ax-mp proj G H G H = proj G H + op proj G H
52 51 eqeq2i proj G = proj G H G H proj G = proj G H + op proj G H
53 coeq2 proj G = proj G H + op proj G H proj H proj G = proj H proj G H + op proj G H
54 48 pjfi proj G H :
55 49 pjfi proj G H :
56 2 54 55 pjsdii proj H proj G H + op proj G H = proj H proj G H + op proj 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 = 0 hop
60 46 59 ax-mp proj H proj G H = 0 hop
61 58 60 oveq12i proj H proj G H + op proj H proj G H = proj G H + op 0 hop
62 54 hoaddid1i proj G H + op 0 hop = proj G H
63 56 61 62 3eqtri proj H proj G H + op proj G H = proj G H
64 63 eqeq2i proj H proj G = proj H proj G H + op proj 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 = 0 hop
70 68 69 ax-mp proj G proj G H = 0 hop
71 65 70 syl6eq proj H proj G = proj G H proj G proj H proj G = 0 hop
72 64 71 sylbi proj H proj G = proj H proj G H + op proj G H proj G proj H proj G = 0 hop
73 53 72 syl proj G = proj G H + op proj G H proj G proj H proj G = 0 hop
74 52 73 sylbi proj G = proj G H G H proj G proj H proj G = 0 hop
75 42 74 syl G = G H G H proj G proj H proj G = 0 hop
76 41 75 sylbi G 𝐶 H proj G proj H proj G = 0 hop
77 38 76 oveq12d G 𝐶 H proj G proj H proj G + op proj G proj H proj G = proj G H + op 0 hop
78 df-iop I op = proj
79 78 coeq2i proj H I op = proj H proj
80 2 pjfi proj H :
81 80 hoid1i proj H I op = proj H
82 79 81 eqtr3i proj H proj = proj H
83 1 pjtoi proj G + op proj G = proj
84 83 coeq2i proj H proj G + op proj G = proj H proj
85 1 pjfi proj G :
86 7 pjfi proj G :
87 2 85 86 pjsdii proj H proj G + op proj G = proj H proj G + op proj H proj G
88 84 87 eqtr3i proj H proj = proj H proj G + op proj H proj G
89 82 88 eqtr3i proj H = proj H proj G + op proj H proj G
90 89 coeq2i proj G proj H = proj G proj H proj G + op proj 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 + op proj H proj G = proj G proj H proj G + op proj G proj H proj G
94 90 93 eqtr2i proj G proj H proj G + op proj G proj H proj G = proj G proj H
95 77 94 27 3eqtr3g G 𝐶 H proj G proj H = proj G H