Metamath Proof Explorer


Theorem pjadjcoi

Description: Adjoint of composition of projections. Special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 6-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 GC
pjco.2 HC
Assertion pjadjcoi ABprojGprojHAihB=AihprojHprojGB

Proof

Step Hyp Ref Expression
1 pjco.1 GC
2 pjco.2 HC
3 2 pjhcli AprojHA
4 1 pjadji projHABprojGprojHAihB=projHAihprojGB
5 3 4 sylan ABprojGprojHAihB=projHAihprojGB
6 1 pjhcli BprojGB
7 2 pjadji AprojGBprojHAihprojGB=AihprojHprojGB
8 6 7 sylan2 ABprojHAihprojGB=AihprojHprojGB
9 5 8 eqtrd ABprojGprojHAihB=AihprojHprojGB
10 1 2 pjcoi AprojGprojHA=projGprojHA
11 10 oveq1d AprojGprojHAihB=projGprojHAihB
12 11 adantr ABprojGprojHAihB=projGprojHAihB
13 2 1 pjcoi BprojHprojGB=projHprojGB
14 13 oveq2d BAihprojHprojGB=AihprojHprojGB
15 14 adantl ABAihprojHprojGB=AihprojHprojGB
16 9 12 15 3eqtr4d ABprojGprojHAihB=AihprojHprojGB