| 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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = ( 𝐺 ‘ 𝑝 ) ↔ 𝐹 = 𝐺 ) ) |