Step | Hyp | Ref
| Expression |
1 | | simp-4l 783 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → 𝐾 ∈ HL) |
2 | | ltrneq.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | eqid 2738 |
. . . . . . . . 9
⊢
(LAut‘𝐾) =
(LAut‘𝐾) |
4 | | ltrneq.t |
. . . . . . . . 9
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
5 | 2, 3, 4 | ltrnlaut 37757 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (LAut‘𝐾)) |
6 | 5 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (LAut‘𝐾)) |
7 | | simpr 488 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
8 | | simplll 775 |
. . . . . . . . . . . . 13
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) ∧ 𝑝 ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
9 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) ∧ 𝑝 ≤ 𝑊) → 𝐹 ∈ 𝑇) |
10 | | ltrneq.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝐾) |
11 | | ltrneq.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = (Atoms‘𝐾) |
12 | 10, 11 | atbase 36923 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵) |
13 | 12 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) ∧ 𝑝 ≤ 𝑊) → 𝑝 ∈ 𝐵) |
14 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) ∧ 𝑝 ≤ 𝑊) → 𝑝 ≤ 𝑊) |
15 | | ltrneq.l |
. . . . . . . . . . . . . 14
⊢ ≤ =
(le‘𝐾) |
16 | 10, 15, 2, 4 | ltrnval1 37768 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ 𝐵 ∧ 𝑝 ≤ 𝑊)) → (𝐹‘𝑝) = 𝑝) |
17 | 8, 9, 13, 14, 16 | syl112anc 1375 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) ∧ 𝑝 ≤ 𝑊) → (𝐹‘𝑝) = 𝑝) |
18 | 17 | ex 416 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) → (𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) |
19 | | pm2.61 195 |
. . . . . . . . . . 11
⊢ ((𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) → ((¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) → (𝐹‘𝑝) = 𝑝)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) → ((¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) → (𝐹‘𝑝) = 𝑝)) |
21 | 20 | ralimdva 3091 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) → ∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = 𝑝)) |
22 | 21 | imp 410 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) → ∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = 𝑝) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → ∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = 𝑝) |
24 | 10, 11, 3 | lauteq 37729 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝐹 ∈ (LAut‘𝐾) ∧ 𝑥 ∈ 𝐵) ∧ ∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = 𝑝) → (𝐹‘𝑥) = 𝑥) |
25 | 1, 6, 7, 23, 24 | syl31anc 1374 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = 𝑥) |
26 | | fvresi 6946 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑥) = 𝑥) |
27 | 26 | adantl 485 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → (( I ↾ 𝐵)‘𝑥) = 𝑥) |
28 | 25, 27 | eqtr4d 2776 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = (( I ↾ 𝐵)‘𝑥)) |
29 | 28 | ralrimiva 3096 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (( I ↾ 𝐵)‘𝑥)) |
30 | 10, 2, 4 | ltrn1o 37758 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵) |
31 | 30 | adantr 484 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) → 𝐹:𝐵–1-1-onto→𝐵) |
32 | | f1ofn 6620 |
. . . . . 6
⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹 Fn 𝐵) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) → 𝐹 Fn 𝐵) |
34 | | fnresi 6466 |
. . . . 5
⊢ ( I
↾ 𝐵) Fn 𝐵 |
35 | | eqfnfv 6810 |
. . . . 5
⊢ ((𝐹 Fn 𝐵 ∧ ( I ↾ 𝐵) Fn 𝐵) → (𝐹 = ( I ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (( I ↾ 𝐵)‘𝑥))) |
36 | 33, 34, 35 | sylancl 589 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) → (𝐹 = ( I ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (( I ↾ 𝐵)‘𝑥))) |
37 | 29, 36 | mpbird 260 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝)) → 𝐹 = ( I ↾ 𝐵)) |
38 | 37 | ex 416 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) → 𝐹 = ( I ↾ 𝐵))) |
39 | 12 | adantl 485 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐵) |
40 | | fvresi 6946 |
. . . . . 6
⊢ (𝑝 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑝) = 𝑝) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) → (( I ↾ 𝐵)‘𝑝) = 𝑝) |
42 | | fveq1 6674 |
. . . . . 6
⊢ (𝐹 = ( I ↾ 𝐵) → (𝐹‘𝑝) = (( I ↾ 𝐵)‘𝑝)) |
43 | 42 | eqeq1d 2740 |
. . . . 5
⊢ (𝐹 = ( I ↾ 𝐵) → ((𝐹‘𝑝) = 𝑝 ↔ (( I ↾ 𝐵)‘𝑝) = 𝑝)) |
44 | 41, 43 | syl5ibrcom 250 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) → (𝐹 = ( I ↾ 𝐵) → (𝐹‘𝑝) = 𝑝)) |
45 | 44 | a1dd 50 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑝 ∈ 𝐴) → (𝐹 = ( I ↾ 𝐵) → (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝))) |
46 | 45 | ralrimdva 3101 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹 = ( I ↾ 𝐵) → ∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝))) |
47 | 38, 46 | impbid 215 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (∀𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 → (𝐹‘𝑝) = 𝑝) ↔ 𝐹 = ( I ↾ 𝐵))) |