trlcone

Description: If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trlcone.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	trlcone.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trlcone.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trlcone.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlcone	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		trlcone.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		trlcone.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		trlcone.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		trlcone.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		simpl3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
6		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
8	2 3	ltrncnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ^◡ 𝐹 ∈ 𝑇 )
9	6 7 8	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ^◡ 𝐹 ∈ 𝑇 )
10		simp12r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
11	2 3	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
12	6 7 10 11	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
13		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
14		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
15	13 14 2 3 4	trlco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ^◡ 𝐹 ∈ 𝑇 ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( ^◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ ^◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
16	6 9 12 15	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ ( ^◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ ^◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
17	1 2 3	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
18	6 7 17	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
19		f1ococnv1	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ( ^◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐵 ) )
20	18 19	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ^◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐵 ) )
21	20	coeq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( ^◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ( I ↾ 𝐵 ) ∘ 𝐺 ) )
22	1 2 3	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
23	6 10 22	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
24		f1of	⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → 𝐺 : 𝐵 ⟶ 𝐵 )
25		fcoi2	⊢ ( 𝐺 : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 )
26	23 24 25	3syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 )
27	21 26	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( ^◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = 𝐺 )
28		coass	⊢ ( ( ^◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ^◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) )
29	27 28	eqtr3di	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 = ( ^◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) )
30	29	fveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ ( ^◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) )
31		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐾 ∈ HL )
32		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) )
33		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
34	14 33	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) )
35	31 32 34	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) )
36	2 3 4	trlcnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ^◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
37	6 7 36	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ ^◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
38	37	eqcomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ^◡ 𝐹 ) )
39		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )
40	38 39	oveq12d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ ^◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
41	35 40	eqtr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑅 ‘ ^◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
42	16 30 41	3brtr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ( le ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) )
43		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
44	31 43	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐾 ∈ AtLat )
45		simp13r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
46	1 33 2 3 4	trlnidat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) )
47	6 10 45 46	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) )
48	13 33	atcmp	⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐺 ) ( le ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) )
49	44 47 32 48	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ( le ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) )
50	42 49	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) )
51	50	eqcomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) )
52	51	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) )
53	52	necon3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
54	5 53	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )
55		simpl3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
56		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
57		simpl2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐺 ∈ 𝑇 )
58		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
59	1 58 2 3 4	trlid0b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝐺 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) )
60	56 57 59	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐺 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) )
61	60	necon3bid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐺 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) ) )
62	55 61	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) )
63	62	necomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 0. ‘ 𝐾 ) ≠ ( 𝑅 ‘ 𝐺 ) )
64		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
65		simpl2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐹 ∈ 𝑇 )
66	1 58 2 3 4	trlid0b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
67	56 65 66	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
68	64 67	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐹 = ( I ↾ 𝐵 ) )
69	68	coeq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = ( ( I ↾ 𝐵 ) ∘ 𝐺 ) )
70	56 57 22	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
71	70 24 25	3syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 )
72	69 71	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = 𝐺 )
73	72	fveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑅 ‘ 𝐺 ) )
74	63 64 73	3netr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )
75		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
76		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → 𝐹 ∈ 𝑇 )
77	58 33 2 3 4	trlator0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
78	75 76 77	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
79	54 74 78	mpjaodan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )

Metamath Proof Explorer

Theorem trlcone

Proof