Metamath Proof Explorer


Theorem pjadj2coi

Description: Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 1-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjadj2co.1 โŠข ๐น โˆˆ Cโ„‹
pjadj2co.2 โŠข ๐บ โˆˆ Cโ„‹
pjadj2co.3 โŠข ๐ป โˆˆ Cโ„‹
Assertion pjadj2coi ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ๐ด ยทih ( ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 pjadj2co.1 โŠข ๐น โˆˆ Cโ„‹
2 pjadj2co.2 โŠข ๐บ โˆˆ Cโ„‹
3 pjadj2co.3 โŠข ๐ป โˆˆ Cโ„‹
4 3 pjhcli โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) โˆˆ โ„‹ )
5 1 2 pjadjcoi โŠข ( ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) )
6 4 5 sylan โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) )
7 2 1 pjcohcli โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) โˆˆ โ„‹ )
8 3 pjadji โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) ) )
9 7 8 sylan2 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) ) )
10 6 9 eqtrd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) ) )
11 1 pjfi โŠข ( projโ„Ž โ€˜ ๐น ) : โ„‹ โŸถ โ„‹
12 2 pjfi โŠข ( projโ„Ž โ€˜ ๐บ ) : โ„‹ โŸถ โ„‹
13 11 12 hocofi โŠข ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) : โ„‹ โŸถ โ„‹
14 3 pjfi โŠข ( projโ„Ž โ€˜ ๐ป ) : โ„‹ โŸถ โ„‹
15 13 14 hocoi โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) = ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) )
16 15 oveq1d โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) )
17 16 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) )
18 coass โŠข ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) = ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) )
19 18 fveq1i โŠข ( ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) ) โ€˜ ๐ต )
20 12 11 hocofi โŠข ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) : โ„‹ โŸถ โ„‹
21 14 20 hocoi โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) ) โ€˜ ๐ต ) = ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) )
22 19 21 eqtrid โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) = ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) )
23 22 oveq2d โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ๐ด ยทih ( ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) ) )
24 23 adantl โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทih ( ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) ) )
25 10 17 24 3eqtr4d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( ( projโ„Ž โ€˜ ๐น ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ๐ด ยทih ( ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โˆ˜ ( projโ„Ž โ€˜ ๐น ) ) โ€˜ ๐ต ) ) )