Metamath Proof Explorer

Theorem pjin2i

Description: Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjin1.1 ⊢G∈Cℋ
pjin1.2 ⊢H∈Cℋ
Assertion pjin2i ⊢projℎ⁡G=projℎ⁡G∘projℎ⁡H∧projℎ⁡H=projℎ⁡H∘projℎ⁡G↔projℎ⁡G=projℎ⁡H

Proof

Step Hyp Ref Expression
1 pjin1.1 ⊢G∈Cℋ
2 pjin1.2 ⊢H∈Cℋ
3 eqss ⊢G=H↔G⊆H∧H⊆G
4 1 2 pjss2coi ⊢G⊆H↔projℎ⁡G∘projℎ⁡H=projℎ⁡G
5 eqcom ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G↔projℎ⁡G=projℎ⁡G∘projℎ⁡H
6 4 5 bitri ⊢G⊆H↔projℎ⁡G=projℎ⁡G∘projℎ⁡H
7 2 1 pjss2coi ⊢H⊆G↔projℎ⁡H∘projℎ⁡G=projℎ⁡H
8 eqcom ⊢projℎ⁡H∘projℎ⁡G=projℎ⁡H↔projℎ⁡H=projℎ⁡H∘projℎ⁡G
9 7 8 bitri ⊢H⊆G↔projℎ⁡H=projℎ⁡H∘projℎ⁡G
10 6 9 anbi12i ⊢G⊆H∧H⊆G↔projℎ⁡G=projℎ⁡G∘projℎ⁡H∧projℎ⁡H=projℎ⁡H∘projℎ⁡G
11 3 10 bitr2i ⊢projℎ⁡G=projℎ⁡G∘projℎ⁡H∧projℎ⁡H=projℎ⁡H∘projℎ⁡G↔G=H
12 fveq2 ⊢G=H→projℎ⁡G=projℎ⁡H
13 11 12 sylbi ⊢projℎ⁡G=projℎ⁡G∘projℎ⁡H∧projℎ⁡H=projℎ⁡H∘projℎ⁡G→projℎ⁡G=projℎ⁡H
14 1 pjidmcoi ⊢projℎ⁡G∘projℎ⁡G=projℎ⁡G
15 coeq2 ⊢projℎ⁡G=projℎ⁡H→projℎ⁡G∘projℎ⁡G=projℎ⁡G∘projℎ⁡H
16 14 15 eqtr3id ⊢projℎ⁡G=projℎ⁡H→projℎ⁡G=projℎ⁡G∘projℎ⁡H
17 coeq2 ⊢projℎ⁡G=projℎ⁡H→projℎ⁡H∘projℎ⁡G=projℎ⁡H∘projℎ⁡H
18 2 pjidmcoi ⊢projℎ⁡H∘projℎ⁡H=projℎ⁡H
19 17 18 eqtr2di ⊢projℎ⁡G=projℎ⁡H→projℎ⁡H=projℎ⁡H∘projℎ⁡G
20 16 19 jca ⊢projℎ⁡G=projℎ⁡H→projℎ⁡G=projℎ⁡G∘projℎ⁡H∧projℎ⁡H=projℎ⁡H∘projℎ⁡G
21 13 20 impbii ⊢projℎ⁡G=projℎ⁡G∘projℎ⁡H∧projℎ⁡H=projℎ⁡H∘projℎ⁡G↔projℎ⁡G=projℎ⁡H