cdlemg47

Description: Part of proof of Lemma G of Crawley p. 116, ninth line of third paragraph on p. 117: "we conclude that gf = fg." (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	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$

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		simp11	$⊢ (((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 (K \in HL \land W \in H)$
6		simp2l	$⊢ (((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 h \in T$
7		simp12	$⊢ (((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 \in T$
8	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land h \in T \land F \in T) \to h \circ F \in T$
9	5 6 7 8	syl3anc	$⊢ (((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 h \circ F \in T$
10		simp13	$⊢ (((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 G \in T$
11		simp3	$⊢ (((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 \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))$
12	1 2 3 4	cdlemg46	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (h \circ F) \neq R (F)$
13	5 7 6 11 12	syl121anc	$⊢ (((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 R (h \circ F) \neq R (F)$
14		simp2r	$⊢ (((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 R (F) = R (G)$
15	13 14	neeqtrd	$⊢ (((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 R (h \circ F) \neq R (G)$
16	2 3 4	cdlemg44	$⊢ ((K \in HL \land W \in H) \land (h \circ F \in T \land G \in T) \land R (h \circ F) \neq R (G)) \to (h \circ F) \circ G = G \circ (h \circ F)$
17	5 9 10 15 16	syl121anc	$⊢ (((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 (h \circ F) \circ G = G \circ (h \circ F)$
18		coass	$⊢ (G \circ h) \circ F = G \circ (h \circ F)$
19	17 18	eqtr4di	$⊢ (((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 (h \circ F) \circ G = (G \circ h) \circ F$
20		simp33	$⊢ (((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 R (h) \neq R (F)$
21	20 14	neeqtrd	$⊢ (((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 R (h) \neq R (G)$
22	2 3 4	cdlemg44	$⊢ ((K \in HL \land W \in H) \land (h \in T \land G \in T) \land R (h) \neq R (G)) \to h \circ G = G \circ h$
23	5 6 10 21 22	syl121anc	$⊢ (((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 h \circ G = G \circ h$
24	23	coeq1d	$⊢ (((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 (h \circ G) \circ F = (G \circ h) \circ F$
25	19 24	eqtr4d	$⊢ (((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 (h \circ F) \circ G = (h \circ G) \circ F$
26		coass	$⊢ (h \circ F) \circ G = h \circ (F \circ G)$
27		coass	$⊢ (h \circ G) \circ F = h \circ (G \circ F)$
28	25 26 27	3eqtr3g	$⊢ (((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 h \circ (F \circ G) = h \circ (G \circ F)$
29	28	coeq2d	$⊢ (((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 h^{-1} \circ (h \circ (F \circ G)) = h^{-1} \circ (h \circ (G \circ F))$
30		coass	$⊢ (h^{-1} \circ h) \circ (F \circ G) = h^{-1} \circ (h \circ (F \circ G))$
31	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land h \in T) \to h : B \underset{1-1 onto}{⟶} B$
32	5 6 31	syl2anc	$⊢ (((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 h : B \underset{1-1 onto}{⟶} B$
33		f1ococnv1	$⊢ h : B \underset{1-1 onto}{⟶} B \to h^{-1} \circ h = {I ↾}_{B}$
34	32 33	syl	$⊢ (((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 h^{-1} \circ h = {I ↾}_{B}$
35	34	coeq1d	$⊢ (((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 (h^{-1} \circ h) \circ (F \circ G) = ({I ↾}_{B}) \circ (F \circ G)$
36	30 35	eqtr3id	$⊢ (((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 h^{-1} \circ (h \circ (F \circ G)) = ({I ↾}_{B}) \circ (F \circ G)$
37	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
38	5 7 10 37	syl3anc	$⊢ (((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 \in T$
39	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \circ G \in T) \to (F \circ G) : B \underset{1-1 onto}{⟶} B$
40	5 38 39	syl2anc	$⊢ (((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) : B \underset{1-1 onto}{⟶} B$
41		f1of	$⊢ (F \circ G) : B \underset{1-1 onto}{⟶} B \to (F \circ G) : B ⟶ B$
42		fcoi2	$⊢ (F \circ G) : B ⟶ B \to ({I ↾}_{B}) \circ (F \circ G) = F \circ G$
43	40 41 42	3syl	$⊢ (((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 ({I ↾}_{B}) \circ (F \circ G) = F \circ G$
44	36 43	eqtrd	$⊢ (((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 h^{-1} \circ (h \circ (F \circ G)) = F \circ G$
45		coass	$⊢ (h^{-1} \circ h) \circ (G \circ F) = h^{-1} \circ (h \circ (G \circ F))$
46	34	coeq1d	$⊢ (((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 (h^{-1} \circ h) \circ (G \circ F) = ({I ↾}_{B}) \circ (G \circ F)$
47	45 46	eqtr3id	$⊢ (((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 h^{-1} \circ (h \circ (G \circ F)) = ({I ↾}_{B}) \circ (G \circ F)$
48	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F \in T) \to G \circ F \in T$
49	5 10 7 48	syl3anc	$⊢ (((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 G \circ F \in T$
50	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \circ F \in T) \to (G \circ F) : B \underset{1-1 onto}{⟶} B$
51	5 49 50	syl2anc	$⊢ (((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 (G \circ F) : B \underset{1-1 onto}{⟶} B$
52		f1of	$⊢ (G \circ F) : B \underset{1-1 onto}{⟶} B \to (G \circ F) : B ⟶ B$
53		fcoi2	$⊢ (G \circ F) : B ⟶ B \to ({I ↾}_{B}) \circ (G \circ F) = G \circ F$
54	51 52 53	3syl	$⊢ (((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 ({I ↾}_{B}) \circ (G \circ F) = G \circ F$
55	47 54	eqtrd	$⊢ (((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 h^{-1} \circ (h \circ (G \circ F)) = G \circ F$
56	29 44 55	3eqtr3d	$⊢ (((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$

Metamath Proof Explorer

Theorem cdlemg47

Proof