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 ⊢ 𝐺 ∈ Cℋ
pjin1.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjin2i ( ( ( projℎ ‘ 𝐺 ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∧ ( projℎ ‘ 𝐻 ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ) ↔ ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) )

Proof

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