Step | Hyp | Ref
| Expression |
1 | | simp1l 1195 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → 𝐾 ∈ 𝑉) |
2 | | ldilco.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | eqid 2759 |
. . . . 5
⊢
(LAut‘𝐾) =
(LAut‘𝐾) |
4 | | ldilco.d |
. . . . 5
⊢ 𝐷 = ((LDil‘𝐾)‘𝑊) |
5 | 2, 3, 4 | ldillaut 37672 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷) → 𝐹 ∈ (LAut‘𝐾)) |
6 | 5 | 3adant3 1130 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → 𝐹 ∈ (LAut‘𝐾)) |
7 | 2, 3, 4 | ldillaut 37672 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝐷) → 𝐺 ∈ (LAut‘𝐾)) |
8 | 7 | 3adant2 1129 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → 𝐺 ∈ (LAut‘𝐾)) |
9 | 3 | lautco 37658 |
. . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ (LAut‘𝐾) ∧ 𝐺 ∈ (LAut‘𝐾)) → (𝐹 ∘ 𝐺) ∈ (LAut‘𝐾)) |
10 | 1, 6, 8, 9 | syl3anc 1369 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘ 𝐺) ∈ (LAut‘𝐾)) |
11 | | simp11 1201 |
. . . . . . . 8
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → (𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻)) |
12 | | simp13 1203 |
. . . . . . . 8
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → 𝐺 ∈ 𝐷) |
13 | | eqid 2759 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
14 | 13, 2, 4 | ldil1o 37673 |
. . . . . . . 8
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝐷) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) |
15 | 11, 12, 14 | syl2anc 588 |
. . . . . . 7
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) |
16 | | f1of 6595 |
. . . . . . 7
⊢ (𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾)) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾)) |
18 | | simp2 1135 |
. . . . . 6
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → 𝑥 ∈ (Base‘𝐾)) |
19 | | fvco3 6744 |
. . . . . 6
⊢ ((𝐺:(Base‘𝐾)⟶(Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥))) |
20 | 17, 18, 19 | syl2anc 588 |
. . . . 5
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥))) |
21 | | simp3 1136 |
. . . . . . 7
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → 𝑥(le‘𝐾)𝑊) |
22 | | eqid 2759 |
. . . . . . . 8
⊢
(le‘𝐾) =
(le‘𝐾) |
23 | 13, 22, 2, 4 | ldilval 37674 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝐷 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊)) → (𝐺‘𝑥) = 𝑥) |
24 | 11, 12, 18, 21, 23 | syl112anc 1372 |
. . . . . 6
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → (𝐺‘𝑥) = 𝑥) |
25 | 24 | fveq2d 6655 |
. . . . 5
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → (𝐹‘(𝐺‘𝑥)) = (𝐹‘𝑥)) |
26 | | simp12 1202 |
. . . . . 6
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → 𝐹 ∈ 𝐷) |
27 | 13, 22, 2, 4 | ldilval 37674 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊)) → (𝐹‘𝑥) = 𝑥) |
28 | 11, 26, 18, 21, 27 | syl112anc 1372 |
. . . . 5
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → (𝐹‘𝑥) = 𝑥) |
29 | 20, 25, 28 | 3eqtrd 2798 |
. . . 4
⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑥(le‘𝐾)𝑊) → ((𝐹 ∘ 𝐺)‘𝑥) = 𝑥) |
30 | 29 | 3exp 1117 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝑥 ∈ (Base‘𝐾) → (𝑥(le‘𝐾)𝑊 → ((𝐹 ∘ 𝐺)‘𝑥) = 𝑥))) |
31 | 30 | ralrimiv 3110 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑊 → ((𝐹 ∘ 𝐺)‘𝑥) = 𝑥)) |
32 | 13, 22, 2, 3, 4 | isldil 37671 |
. . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ((𝐹 ∘ 𝐺) ∈ 𝐷 ↔ ((𝐹 ∘ 𝐺) ∈ (LAut‘𝐾) ∧ ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑊 → ((𝐹 ∘ 𝐺)‘𝑥) = 𝑥)))) |
33 | 32 | 3ad2ant1 1131 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → ((𝐹 ∘ 𝐺) ∈ 𝐷 ↔ ((𝐹 ∘ 𝐺) ∈ (LAut‘𝐾) ∧ ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑊 → ((𝐹 ∘ 𝐺)‘𝑥) = 𝑥)))) |
34 | 10, 31, 33 | mpbir2and 713 |
1
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷) → (𝐹 ∘ 𝐺) ∈ 𝐷) |