Metamath Proof Explorer

Theorem cdlemg47a

Description: TODO: fix comment. TODO: Use this above in place of ( FP ) = P antecedents? (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses cdlemg46.b ⊢ B = Base K
cdlemg46.h ⊢ H = LHyp ⁡ K
cdlemg46.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion cdlemg47a ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → F ∘ G = G ∘ F

Proof

Step Hyp Ref Expression
1 cdlemg46.b ⊢ B = Base K
2 cdlemg46.h ⊢ H = LHyp ⁡ K
3 cdlemg46.t ⊢ T = LTrn ⁡ K ⁡ W
4 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → K ∈ HL ∧ W ∈ H
5 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → G ∈ T
6 1 2 3 ltrn1o ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T → G : B ⟶ 1-1 onto B
7 4 5 6 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → G : B ⟶ 1-1 onto B
8 f1of ⊢ G : B ⟶ 1-1 onto B → G : B ⟶ B
9 7 8 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → G : B ⟶ B
10 fcoi1 ⊢ G : B ⟶ B → G ∘ I ↾ B = G
11 9 10 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → G ∘ I ↾ B = G
12 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → F = I ↾ B
13 12 coeq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → G ∘ F = G ∘ I ↾ B
14 12 coeq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → F ∘ G = I ↾ B ∘ G
15 fcoi2 ⊢ G : B ⟶ B → I ↾ B ∘ G = G
16 9 15 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → I ↾ B ∘ G = G
17 14 16 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → F ∘ G = G
18 11 13 17 3eqtr4rd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ F = I ↾ B → F ∘ G = G ∘ F