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โ โ ๐น ) ) โ ๐ต ) ) ) |