Theorem 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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemg46.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemg46.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemg46.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	cdlemg47	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemg46.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemg46.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		cdlemg46.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		cdlemg46.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ℎ ∈ 𝑇 )
7		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → 𝐹 ∈ 𝑇 )
8	2 3	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ℎ ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( ℎ ∘ 𝐹 ) ∈ 𝑇 )
9	5 6 7 8	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ℎ ∘ 𝐹 ) ∈ 𝑇 )
10		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → 𝐺 ∈ 𝑇 )
11		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) )
12	1 2 3 4	cdlemg46	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ ( ℎ ∘ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐹 ) )
13	5 7 6 11 12	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ ( ℎ ∘ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐹 ) )
14		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) )
15	13 14	neeqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ ( ℎ ∘ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐺 ) )
16	2 3 4	cdlemg44	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ℎ ∘ 𝐹 ) ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ ( ℎ ∘ 𝐹 ) ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( ( ℎ ∘ 𝐹 ) ∘ 𝐺 ) = ( 𝐺 ∘ ( ℎ ∘ 𝐹 ) ) )
17	5 9 10 15 16	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( ℎ ∘ 𝐹 ) ∘ 𝐺 ) = ( 𝐺 ∘ ( ℎ ∘ 𝐹 ) ) )
18		coass	⊢ ( ( 𝐺 ∘ ℎ ) ∘ 𝐹 ) = ( 𝐺 ∘ ( ℎ ∘ 𝐹 ) )
19	17 18	eqtr4di	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( ℎ ∘ 𝐹 ) ∘ 𝐺 ) = ( ( 𝐺 ∘ ℎ ) ∘ 𝐹 ) )
20		simp33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) )
21	20 14	neeqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐺 ) )
22	2 3 4	cdlemg44	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( ℎ ∘ 𝐺 ) = ( 𝐺 ∘ ℎ ) )
23	5 6 10 21 22	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ℎ ∘ 𝐺 ) = ( 𝐺 ∘ ℎ ) )
24	23	coeq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( ℎ ∘ 𝐺 ) ∘ 𝐹 ) = ( ( 𝐺 ∘ ℎ ) ∘ 𝐹 ) )
25	19 24	eqtr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( ℎ ∘ 𝐹 ) ∘ 𝐺 ) = ( ( ℎ ∘ 𝐺 ) ∘ 𝐹 ) )
26		coass	⊢ ( ( ℎ ∘ 𝐹 ) ∘ 𝐺 ) = ( ℎ ∘ ( 𝐹 ∘ 𝐺 ) )
27		coass	⊢ ( ( ℎ ∘ 𝐺 ) ∘ 𝐹 ) = ( ℎ ∘ ( 𝐺 ∘ 𝐹 ) )
28	25 26 27	3eqtr3g	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ℎ ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ℎ ∘ ( 𝐺 ∘ 𝐹 ) ) )
29	28	coeq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐺 ∘ 𝐹 ) ) ) )
30		coass	⊢ ( ( ◡ ℎ ∘ ℎ ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐹 ∘ 𝐺 ) ) )
31	1 2 3	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ℎ ∈ 𝑇 ) → ℎ : 𝐵 –1-1-onto→ 𝐵 )
32	5 6 31	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ℎ : 𝐵 –1-1-onto→ 𝐵 )
33		f1ococnv1	⊢ ( ℎ : 𝐵 –1-1-onto→ 𝐵 → ( ◡ ℎ ∘ ℎ ) = ( I ↾ 𝐵 ) )
34	32 33	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ◡ ℎ ∘ ℎ ) = ( I ↾ 𝐵 ) )
35	34	coeq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( ◡ ℎ ∘ ℎ ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝐹 ∘ 𝐺 ) ) )
36	30 35	eqtr3id	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝐹 ∘ 𝐺 ) ) )
37	2 3	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
38	5 7 10 37	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
39	1 2 3	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 )
40	5 38 39	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐹 ∘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 )
41		f1of	⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 → ( 𝐹 ∘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
42		fcoi2	⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝐹 ∘ 𝐺 ) )
43	40 41 42	3syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( I ↾ 𝐵 ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝐹 ∘ 𝐺 ) )
44	36 43	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐹 ∘ 𝐺 ) ) ) = ( 𝐹 ∘ 𝐺 ) )
45		coass	⊢ ( ( ◡ ℎ ∘ ℎ ) ∘ ( 𝐺 ∘ 𝐹 ) ) = ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐺 ∘ 𝐹 ) ) )
46	34	coeq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( ◡ ℎ ∘ ℎ ) ∘ ( 𝐺 ∘ 𝐹 ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝐺 ∘ 𝐹 ) ) )
47	45 46	eqtr3id	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐺 ∘ 𝐹 ) ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝐺 ∘ 𝐹 ) ) )
48	2 3	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ 𝐹 ) ∈ 𝑇 )
49	5 10 7 48	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ 𝑇 )
50	1 2 3	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ 𝐹 ) ∈ 𝑇 ) → ( 𝐺 ∘ 𝐹 ) : 𝐵 –1-1-onto→ 𝐵 )
51	5 49 50	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐺 ∘ 𝐹 ) : 𝐵 –1-1-onto→ 𝐵 )
52		f1of	⊢ ( ( 𝐺 ∘ 𝐹 ) : 𝐵 –1-1-onto→ 𝐵 → ( 𝐺 ∘ 𝐹 ) : 𝐵 ⟶ 𝐵 )
53		fcoi2	⊢ ( ( 𝐺 ∘ 𝐹 ) : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ∘ 𝐹 ) )
54	51 52 53	3syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( I ↾ 𝐵 ) ∘ ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ∘ 𝐹 ) )
55	47 54	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ◡ ℎ ∘ ( ℎ ∘ ( 𝐺 ∘ 𝐹 ) ) ) = ( 𝐺 ∘ 𝐹 ) )
56	29 44 55	3eqtr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ℎ ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ ℎ ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) )