Metamath Proof Explorer


Theorem pjci

Description: Two subspaces commute iff their projections commute. Lemma 4 of Kalmbach p. 67. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 G C
pjclem1.2 H C
Assertion pjci G 𝐶 H proj G proj H = proj H proj G

Proof

Step Hyp Ref Expression
1 pjclem1.1 G C
2 pjclem1.2 H C
3 1 2 pjclem2 G 𝐶 H proj G proj H = proj H proj G
4 1 2 pjclem4 proj G proj H = proj H proj G proj G proj H = proj G H
5 1 2 pjclem3 proj G proj H = proj H proj G proj G proj H = proj H proj G
6 2 choccli H C
7 1 6 pjclem4 proj G proj H = proj H proj G proj G proj H = proj G H
8 5 7 syl proj G proj H = proj H proj G proj G proj H = proj G H
9 4 8 oveq12d proj G proj H = proj H proj G proj G proj H + op proj G proj H = proj G H + op proj G H
10 df-iop I op = proj
11 10 coeq2i proj G I op = proj G proj
12 1 pjfi proj G :
13 12 hoid1i proj G I op = proj G
14 11 13 eqtr3i proj G proj = proj G
15 2 pjtoi proj H + op proj H = proj
16 15 coeq2i proj G proj H + op proj H = proj G proj
17 2 pjfi proj H :
18 6 pjfi proj H :
19 1 17 18 pjsdii proj G proj H + op proj H = proj G proj H + op proj G proj H
20 16 19 eqtr3i proj G proj = proj G proj H + op proj G proj H
21 14 20 eqtr3i proj G = proj G proj H + op proj G proj H
22 inss2 G H H
23 1 choccli G C
24 2 23 chub2i H G H
25 22 24 sstri G H G H
26 1 2 chdmm3i G H = G H
27 25 26 sseqtrri G H G H
28 1 2 chincli G H C
29 1 6 chincli G H C
30 28 29 pjscji G H G H proj G H G H = proj G H + op proj G H
31 27 30 ax-mp proj G H G H = proj G H + op proj G H
32 9 21 31 3eqtr4g proj G proj H = proj H proj G proj G = proj G H G H
33 28 29 chjcli G H G H C
34 1 33 pj11i proj G = proj G H G H G = G H G H
35 32 34 sylib proj G proj H = proj H proj G G = G H G H
36 1 2 cmbri G 𝐶 H G = G H G H
37 35 36 sylibr proj G proj H = proj H proj G G 𝐶 H
38 3 37 impbii G 𝐶 H proj G proj H = proj H proj G