Theorem pjcmul2i

Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 1 of AkhiezerGlazman p. 65. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjclem1.1	⊢ 𝐺 ∈ Cℋ
	pjclem1.2	⊢ 𝐻 ∈ Cℋ
Assertion	pjcmul2i	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	⊢ 𝐺 ∈ Cℋ
2		pjclem1.2	⊢ 𝐻 ∈ Cℋ
3	1 2	pjclem4	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )
4		pjmfn	⊢ projℎ Fn Cℋ
5	1 2	chincli	⊢ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ
6		fnfvelrn	⊢ ( ( projℎ Fn Cℋ ∧ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ ) → ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ∈ ran projℎ )
7	4 5 6	mp2an	⊢ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ∈ ran projℎ
8		eleq1	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ ↔ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ∈ ran projℎ ) )
9	7 8	mpbiri	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ )
10	1 2	pjcmul1i	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ )
11	9 10	sylibr	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )
12	3 11	impbii	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )