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 โŠข ๐บ โˆˆ Cโ„‹
pjco.2 โŠข ๐ป โˆˆ Cโ„‹
Assertion pjadjcoi ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ๐ด ยทih ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 โŠข ๐บ โˆˆ Cโ„‹
2 pjco.2 โŠข ๐ป โˆˆ Cโ„‹
3 2 pjhcli โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) โˆˆ โ„‹ )
4 1 pjadji โŠข ( ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) )
5 3 4 sylan โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) )
6 1 pjhcli โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) โˆˆ โ„‹ )
7 2 pjadji โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) ) )
8 6 7 sylan2 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ยทih ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) ) )
9 5 8 eqtrd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) ) )
10 1 2 pjcoi โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) = ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) )
11 10 oveq1d โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) )
12 11 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ๐ด ) ) ยทih ๐ต ) )
13 2 1 pjcoi โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ๐ต ) = ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) )
14 13 oveq2d โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( ๐ด ยทih ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) ) )
15 14 adantl โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทih ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ๐ต ) ) = ( ๐ด ยทih ( ( projโ„Ž โ€˜ ๐ป ) โ€˜ ( ( projโ„Ž โ€˜ ๐บ ) โ€˜ ๐ต ) ) ) )
16 9 12 15 3eqtr4d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ๐บ ) โˆ˜ ( projโ„Ž โ€˜ ๐ป ) ) โ€˜ ๐ด ) ยทih ๐ต ) = ( ๐ด ยทih ( ( ( projโ„Ž โ€˜ ๐ป ) โˆ˜ ( projโ„Ž โ€˜ ๐บ ) ) โ€˜ ๐ต ) ) )