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 \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to F \circ G = G \circ 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 \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to (K \in HL \land W \in H)$
5		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to G \in T$
6	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : B \underset{1-1 onto}{⟶} B$
7	4 5 6	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to G : B \underset{1-1 onto}{⟶} B$
8		f1of	$⊢ G : B \underset{1-1 onto}{⟶} B \to G : B ⟶ B$
9	7 8	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to G : B ⟶ B$
10		fcoi1	$⊢ G : B ⟶ B \to G \circ ({I ↾}_{B}) = G$
11	9 10	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to G \circ ({I ↾}_{B}) = G$
12		simp3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to F = {I ↾}_{B}$
13	12	coeq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to G \circ F = G \circ ({I ↾}_{B})$
14	12	coeq1d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to F \circ G = ({I ↾}_{B}) \circ G$
15		fcoi2	$⊢ G : B ⟶ B \to ({I ↾}_{B}) \circ G = G$
16	9 15	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to ({I ↾}_{B}) \circ G = G$
17	14 16	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to F \circ G = G$
18	11 13 17	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{B}) \to F \circ G = G \circ F$