Metamath Proof Explorer

Theorem cdlemg48

Description: Eliminate h from cdlemg47 . (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)$
		cdlemg46.r	$⊢ R = trL (K) (W)$
	Assertion	cdlemg48	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \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		cdlemg46.r	$⊢ R = trL (K) (W)$
5	1 2 3 4	cdlemftr1	$⊢ (K \in HL \land W \in H) \to \exists h \in T (h \neq {I ↾}_{B} \land R (h) \neq R (F))$
6	5	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \to \exists h \in T (h \neq {I ↾}_{B} \land R (h) \neq R (F))$
7		simp11	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to (K \in HL \land W \in H)$
8		simp12l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \in T$
9		simp12r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to G \in T$
10		simp2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \in T$
11		simp13r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (F) = R (G)$
12		simp13l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \neq {I ↾}_{B}$
13		simp3l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \neq {I ↾}_{B}$
14		simp3r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (h) \neq R (F)$
15	1 2 3 4	cdlemg47	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (h \in T \land R (F) = R (G)) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \circ G = G \circ F$
16	7 8 9 10 11 12 13 14 15	syl323anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \land h \in T \land (h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \circ G = G \circ F$
17	16	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \to (\exists h \in T (h \neq {I ↾}_{B} \land R (h) \neq R (F)) \to F \circ G = G \circ F)$
18	6 17	mpd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{B} \land R (F) = R (G))) \to F \circ G = G \circ F$