This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltrneq2

Description: The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014)

Ref Expression
Hypotheses ltrneq2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ltrneq2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrneq2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrneq2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ 𝐹 = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ltrneq2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 ltrneq2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 ltrneq2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐺 ∈ 𝑇 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
8 4 5 7 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
9 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐹 ∈ 𝑇 )
10 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝑞 ∈ 𝐴 )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 11 1 2 3 ltrncnvat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑞 ∈ 𝐴 ) → ( ◡ 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
13 4 9 10 12 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
14 6 1 atbase ⊢ ( ( ◡ 𝐹 ‘ 𝑞 ) ∈ 𝐴 → ( ◡ 𝐹 ‘ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐹 ‘ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
16 f1ocnvfv1 ⊢ ( ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐹 ‘ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) ) = ( ◡ 𝐹 ‘ 𝑞 ) )
17 8 15 16 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) ) = ( ◡ 𝐹 ‘ 𝑞 ) )
18 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) )
19 fveq2 ⊢ ( 𝑝 = ( ◡ 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) )
20 fveq2 ⊢ ( 𝑝 = ( ◡ 𝐹 ‘ 𝑞 ) → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) )
21 19 20 eqeq12d ⊢ ( 𝑝 = ( ◡ 𝐹 ‘ 𝑞 ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) = ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) ) )
22 21 rspcv ⊢ ( ( ◡ 𝐹 ‘ 𝑞 ) ∈ 𝐴 → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) = ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) ) )
23 13 18 22 sylc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) = ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) )
24 6 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
25 4 9 24 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
26 6 1 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
27 10 26 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
28 f1ocnvfv2 ⊢ ( ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) = 𝑞 )
29 25 27 28 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) = 𝑞 )
30 23 29 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) = 𝑞 )
31 30 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ ( ◡ 𝐹 ‘ 𝑞 ) ) ) = ( ◡ 𝐺 ‘ 𝑞 ) )
32 17 31 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐹 ‘ 𝑞 ) = ( ◡ 𝐺 ‘ 𝑞 ) )
33 32 breq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ( ◡ 𝐹 ‘ 𝑞 ) ( le ‘ 𝐾 ) 𝑥 ↔ ( ◡ 𝐺 ‘ 𝑞 ) ( le ‘ 𝐾 ) 𝑥 ) )
34 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
35 f1ocnvfv1 ⊢ ( ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
36 25 34 35 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
37 36 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ( ◡ 𝐹 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ◡ 𝐹 ‘ 𝑞 ) ( le ‘ 𝐾 ) 𝑥 ) )
38 f1ocnvfv1 ⊢ ( ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) = 𝑥 )
39 8 34 38 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) = 𝑥 )
40 39 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ( ◡ 𝐺 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ↔ ( ◡ 𝐺 ‘ 𝑞 ) ( le ‘ 𝐾 ) 𝑥 ) )
41 33 37 40 3bitr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( ( ◡ 𝐹 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ◡ 𝐺 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
42 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
43 eqid ⊢ ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
44 2 43 3 ltrnlaut ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
45 4 9 44 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
46 6 2 3 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
47 4 9 34 46 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
48 6 11 43 lautcnvle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ ( LAut ‘ 𝐾 ) ) ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ ( ◡ 𝐹 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
49 42 45 27 47 48 syl22anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ ( ◡ 𝐹 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
50 2 43 3 ltrnlaut ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 ∈ ( LAut ‘ 𝐾 ) )
51 4 5 50 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → 𝐺 ∈ ( LAut ‘ 𝐾 ) )
52 6 2 3 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
53 4 5 34 52 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
54 6 11 43 lautcnvle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐺 ∈ ( LAut ‘ 𝐾 ) ) ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ↔ ( ◡ 𝐺 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
55 42 51 27 53 54 syl22anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ↔ ( ◡ 𝐺 ‘ 𝑞 ) ( le ‘ 𝐾 ) ( ◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
56 41 49 55 3bitr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ) )
57 56 3exp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → ( 𝑞 ∈ 𝐴 → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
58 57 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → ( 𝑞 ∈ 𝐴 → ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ) ) ) )
59 58 ralrimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → ∀ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ) ) )
60 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ HL )
61 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
62 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐹 ∈ 𝑇 )
63 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
64 61 62 63 46 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
65 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐺 ∈ 𝑇 )
66 61 65 63 52 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
67 6 11 1 hlateq ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
68 60 64 66 67 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑞 ∈ 𝐴 ( 𝑞 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
69 59 68 sylibd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
70 69 ralrimdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
71 24 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
72 f1ofn ⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐹 Fn ( Base ‘ 𝐾 ) )
73 71 72 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐹 Fn ( Base ‘ 𝐾 ) )
74 7 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
75 f1ofn ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 Fn ( Base ‘ 𝐾 ) )
76 74 75 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐺 Fn ( Base ‘ 𝐾 ) )
77 eqfnfv ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐾 ) ∧ 𝐺 Fn ( Base ‘ 𝐾 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
78 73 76 77 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
79 70 78 sylibrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) → 𝐹 = 𝐺 ) )
80 fveq1 ⊢ ( 𝐹 = 𝐺 → ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) )
81 80 ralrimivw ⊢ ( 𝐹 = 𝐺 → ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) )
82 79 81 impbid1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ 𝐹 = 𝐺 ) )