ltrncom

Description: Composition is commutative for translations. Part of proof of Lemma G of Crawley p. 116. (Contributed by NM, 5-Jun-2013)

	Ref	Expression
Hypotheses	ltrncom.h	$⊢ H = LHyp (K)$
	ltrncom.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrncom	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G = G \circ F$

Proof

Step	Hyp	Ref	Expression
1		ltrncom.h	$⊢ H = LHyp (K)$
2		ltrncom.t	$⊢ T = LTrn (K) (W)$
3		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to (K \in HL \land W \in H)$
4		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to F \in T$
5		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to G \in T$
6		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to F = {I ↾}_{{Base}_{K}}$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 1 2	cdlemg47a	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to F \circ G = G \circ F$
9	3 4 5 6 8	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to F \circ G = G \circ F$
10		simpll1	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) = trL (K) (W) (G)) \to (K \in HL \land W \in H)$
11		simpll2	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) = trL (K) (W) (G)) \to F \in T$
12		simpll3	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) = trL (K) (W) (G)) \to G \in T$
13		simplr	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) = trL (K) (W) (G)) \to F \neq {I ↾}_{{Base}_{K}}$
14		simpr	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) = trL (K) (W) (G)) \to trL (K) (W) (F) = trL (K) (W) (G)$
15		eqid	$⊢ trL (K) (W) = trL (K) (W)$
16	7 1 2 15	cdlemg48	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land trL (K) (W) (F) = trL (K) (W) (G))) \to F \circ G = G \circ F$
17	10 11 12 13 14 16	syl122anc	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) = trL (K) (W) (G)) \to F \circ G = G \circ F$
18		simpll1	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) \neq trL (K) (W) (G)) \to (K \in HL \land W \in H)$
19		simpll2	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) \neq trL (K) (W) (G)) \to F \in T$
20		simpll3	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) \neq trL (K) (W) (G)) \to G \in T$
21		simpr	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) \neq trL (K) (W) (G)) \to trL (K) (W) (F) \neq trL (K) (W) (G)$
22	1 2 15	cdlemg44	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land trL (K) (W) (F) \neq trL (K) (W) (G)) \to F \circ G = G \circ F$
23	18 19 20 21 22	syl121anc	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \land trL (K) (W) (F) \neq trL (K) (W) (G)) \to F \circ G = G \circ F$
24	17 23	pm2.61dane	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \neq {I ↾}_{{Base}_{K}}) \to F \circ G = G \circ F$
25	9 24	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G = G \circ F$

Metamath Proof Explorer

Theorem ltrncom

Proof