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ℎ ‘ 𝐺 ) ) ‘ 𝐵 ) ) )