| Step | Hyp | Ref
| Expression |
| 1 | | chsh 31243 |
. . . . . . . 8
⊢ (𝐻 ∈
Cℋ → 𝐻 ∈ Sℋ
) |
| 2 | | shocsh 31303 |
. . . . . . . 8
⊢ (𝐻 ∈
Sℋ → (⊥‘𝐻) ∈ Sℋ
) |
| 3 | | shsel 31333 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ (⊥‘𝐻) ∈ Sℋ )
→ (𝐴 ∈ (𝐻 +ℋ
(⊥‘𝐻)) ↔
∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 4 | 1, 2, 3 | syl2anc2 585 |
. . . . . . 7
⊢ (𝐻 ∈
Cℋ → (𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻)) ↔ ∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 5 | 4 | biimpa 476 |
. . . . . 6
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) |
| 6 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝐻 ∈
Cℋ → (⊥‘𝐻) ∈ Sℋ
) |
| 7 | | ocin 31315 |
. . . . . . . . 9
⊢ (𝐻 ∈
Sℋ → (𝐻 ∩ (⊥‘𝐻)) = 0ℋ) |
| 8 | 1, 7 | syl 17 |
. . . . . . . 8
⊢ (𝐻 ∈
Cℋ → (𝐻 ∩ (⊥‘𝐻)) = 0ℋ) |
| 9 | | pjhthmo 31321 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ (⊥‘𝐻) ∈ Sℋ
∧ (𝐻 ∩
(⊥‘𝐻)) =
0ℋ) → ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 10 | 1, 6, 8, 9 | syl3anc 1373 |
. . . . . . 7
⊢ (𝐻 ∈
Cℋ → ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 12 | | reu5 3382 |
. . . . . . 7
⊢
(∃!𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ (∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 13 | | df-rmo 3380 |
. . . . . . . 8
⊢
(∃*𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 14 | 13 | anbi2i 623 |
. . . . . . 7
⊢
((∃𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ↔ (∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)))) |
| 15 | 12, 14 | bitri 275 |
. . . . . 6
⊢
(∃!𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ (∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)))) |
| 16 | 5, 11, 15 | sylanbrc 583 |
. . . . 5
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ∃!𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) |
| 17 | | riotacl 7405 |
. . . . 5
⊢
(∃!𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) → (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ∈ 𝐻) |
| 18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ∈ 𝐻) |
| 19 | | eleq1 2829 |
. . . 4
⊢
((℩𝑦
∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵 → ((℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ∈ 𝐻 ↔ 𝐵 ∈ 𝐻)) |
| 20 | 18, 19 | syl5ibcom 245 |
. . 3
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ((℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵 → 𝐵 ∈ 𝐻)) |
| 21 | 20 | pm4.71rd 562 |
. 2
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ((℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵))) |
| 22 | | shsss 31332 |
. . . . . 6
⊢ ((𝐻 ∈
Sℋ ∧ (⊥‘𝐻) ∈ Sℋ )
→ (𝐻
+ℋ (⊥‘𝐻)) ⊆ ℋ) |
| 23 | 1, 2, 22 | syl2anc2 585 |
. . . . 5
⊢ (𝐻 ∈
Cℋ → (𝐻 +ℋ (⊥‘𝐻)) ⊆
ℋ) |
| 24 | 23 | sselda 3983 |
. . . 4
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → 𝐴 ∈ ℋ) |
| 25 | | pjhval 31416 |
. . . 4
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ ℋ) →
((projℎ‘𝐻)‘𝐴) = (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 26 | 24, 25 | syldan 591 |
. . 3
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) →
((projℎ‘𝐻)‘𝐴) = (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
| 27 | 26 | eqeq1d 2739 |
. 2
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) →
(((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵)) |
| 28 | | id 22 |
. . . 4
⊢ (𝐵 ∈ 𝐻 → 𝐵 ∈ 𝐻) |
| 29 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 +ℎ 𝑥) = (𝐵 +ℎ 𝑥)) |
| 30 | 29 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 = (𝑦 +ℎ 𝑥) ↔ 𝐴 = (𝐵 +ℎ 𝑥))) |
| 31 | 30 | rexbidv 3179 |
. . . . 5
⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥))) |
| 32 | 31 | riota2 7413 |
. . . 4
⊢ ((𝐵 ∈ 𝐻 ∧ ∃!𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) → (∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥) ↔ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵)) |
| 33 | 28, 16, 32 | syl2anr 597 |
. . 3
⊢ (((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) ∧ 𝐵 ∈ 𝐻) → (∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥) ↔ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵)) |
| 34 | 33 | pm5.32da 579 |
. 2
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ((𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)) ↔ (𝐵 ∈ 𝐻 ∧ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵))) |
| 35 | 21, 27, 34 | 3bitr4d 311 |
1
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) →
(((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)))) |