Metamath Proof Explorer


Theorem pjclem4

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

Ref Expression
Hypotheses pjclem1.1 GC
pjclem1.2 HC
Assertion pjclem4 projGprojH=projHprojGprojGprojH=projGH

Proof

Step Hyp Ref Expression
1 pjclem1.1 GC
2 pjclem1.2 HC
3 1 2 pjcocli xprojGprojHxG
4 3 adantl projGprojH=projHprojGxprojGprojHxG
5 2 1 pjcocli xprojHprojGxH
6 fveq1 projGprojH=projHprojGprojGprojHx=projHprojGx
7 6 eleq1d projGprojH=projHprojGprojGprojHxHprojHprojGxH
8 5 7 syl5ibr projGprojH=projHprojGxprojGprojHxH
9 8 imp projGprojH=projHprojGxprojGprojHxH
10 4 9 elind projGprojH=projHprojGxprojGprojHxGH
11 1 2 pjcohcli xprojGprojHx
12 hvsubcl xprojGprojHxx-projGprojHx
13 11 12 mpdan xx-projGprojHx
14 13 adantl projGprojH=projHprojGxx-projGprojHx
15 simpl xyGHx
16 11 adantr xyGHprojGprojHx
17 1 2 chincli GHC
18 17 cheli yGHy
19 18 adantl xyGHy
20 15 16 19 3jca xyGHxprojGprojHxy
21 20 adantl projGprojH=projHprojGxyGHxprojGprojHxy
22 his2sub xprojGprojHxyx-projGprojHxihy=xihyprojGprojHxihy
23 21 22 syl projGprojH=projHprojGxyGHx-projGprojHxihy=xihyprojGprojHxihy
24 6 oveq1d projGprojH=projHprojGprojGprojHxihy=projHprojGxihy
25 2 1 pjadjcoi xyprojHprojGxihy=xihprojGprojHy
26 18 25 sylan2 xyGHprojHprojGxihy=xihprojGprojHy
27 1 2 pjclem4a yGHprojGprojHy=y
28 27 oveq2d yGHxihprojGprojHy=xihy
29 28 adantl xyGHxihprojGprojHy=xihy
30 26 29 eqtrd xyGHprojHprojGxihy=xihy
31 24 30 sylan9eq projGprojH=projHprojGxyGHprojGprojHxihy=xihy
32 31 oveq1d projGprojH=projHprojGxyGHprojGprojHxihyprojGprojHxihy=xihyprojGprojHxihy
33 11 18 anim12i xyGHprojGprojHxy
34 33 adantl projGprojH=projHprojGxyGHprojGprojHxy
35 hicl projGprojHxyprojGprojHxihy
36 34 35 syl projGprojH=projHprojGxyGHprojGprojHxihy
37 36 subidd projGprojH=projHprojGxyGHprojGprojHxihyprojGprojHxihy=0
38 23 32 37 3eqtr2d projGprojH=projHprojGxyGHx-projGprojHxihy=0
39 38 expr projGprojH=projHprojGxyGHx-projGprojHxihy=0
40 39 ralrimiv projGprojH=projHprojGxyGHx-projGprojHxihy=0
41 17 chshii GHS
42 shocel GHSx-projGprojHxGHx-projGprojHxyGHx-projGprojHxihy=0
43 41 42 ax-mp x-projGprojHxGHx-projGprojHxyGHx-projGprojHxihy=0
44 14 40 43 sylanbrc projGprojH=projHprojGxx-projGprojHxGH
45 17 pjvi projGprojHxGHx-projGprojHxGHprojGHprojGprojHx+x-projGprojHx=projGprojHx
46 10 44 45 syl2anc projGprojH=projHprojGxprojGHprojGprojHx+x-projGprojHx=projGprojHx
47 id xx
48 hvaddsub12 projGprojHxxprojGprojHxprojGprojHx+x-projGprojHx=x+projGprojHx-projGprojHx
49 11 47 11 48 syl3anc xprojGprojHx+x-projGprojHx=x+projGprojHx-projGprojHx
50 hvsubid projGprojHxprojGprojHx-projGprojHx=0
51 11 50 syl xprojGprojHx-projGprojHx=0
52 51 oveq2d xx+projGprojHx-projGprojHx=x+0
53 ax-hvaddid xx+0=x
54 49 52 53 3eqtrd xprojGprojHx+x-projGprojHx=x
55 54 fveq2d xprojGHprojGprojHx+x-projGprojHx=projGHx
56 55 adantl projGprojH=projHprojGxprojGHprojGprojHx+x-projGprojHx=projGHx
57 46 56 eqtr3d projGprojH=projHprojGxprojGprojHx=projGHx
58 57 ralrimiva projGprojH=projHprojGxprojGprojHx=projGHx
59 1 pjfi projG:
60 2 pjfi projH:
61 59 60 hocofi projGprojH:
62 17 pjfi projGH:
63 61 62 hoeqi xprojGprojHx=projGHxprojGprojH=projGH
64 58 63 sylib projGprojH=projHprojGprojGprojH=projGH