Step | Hyp | Ref
| Expression |
1 | | chsh 28081 |
. . . . . . . 8
⊢ (𝐻 ∈
Cℋ → 𝐻 ∈ Sℋ
) |
2 | | shocsh 28143 |
. . . . . . . . 9
⊢ (𝐻 ∈
Sℋ → (⊥‘𝐻) ∈ Sℋ
) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝐻 ∈
Cℋ → (⊥‘𝐻) ∈ Sℋ
) |
4 | | shsel 28173 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ (⊥‘𝐻) ∈ Sℋ )
→ (𝐴 ∈ (𝐻 +ℋ
(⊥‘𝐻)) ↔
∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
5 | 1, 3, 4 | syl2anc 693 |
. . . . . . 7
⊢ (𝐻 ∈
Cℋ → (𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻)) ↔ ∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
6 | 5 | biimpa 501 |
. . . . . 6
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) |
7 | | ocin 28155 |
. . . . . . . . 9
⊢ (𝐻 ∈
Sℋ → (𝐻 ∩ (⊥‘𝐻)) = 0ℋ) |
8 | 1, 7 | syl 17 |
. . . . . . . 8
⊢ (𝐻 ∈
Cℋ → (𝐻 ∩ (⊥‘𝐻)) = 0ℋ) |
9 | | pjhthmo 28161 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ (⊥‘𝐻) ∈ Sℋ
∧ (𝐻 ∩
(⊥‘𝐻)) =
0ℋ) → ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
10 | 1, 3, 8, 9 | syl3anc 1326 |
. . . . . . 7
⊢ (𝐻 ∈
Cℋ → ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
11 | 10 | adantr 481 |
. . . . . 6
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
12 | | reu5 3159 |
. . . . . . 7
⊢
(∃!𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ (∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
13 | | df-rmo 2920 |
. . . . . . . 8
⊢
(∃*𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
14 | 13 | anbi2i 730 |
. . . . . . 7
⊢
((∃𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ↔ (∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)))) |
15 | 12, 14 | bitri 264 |
. . . . . 6
⊢
(∃!𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ (∃𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ∧ ∃*𝑦(𝑦 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)))) |
16 | 6, 11, 15 | sylanbrc 698 |
. . . . 5
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ∃!𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) |
17 | | riotacl 6625 |
. . . . 5
⊢
(∃!𝑦 ∈
𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) → (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ∈ 𝐻) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ∈ 𝐻) |
19 | | eleq1 2689 |
. . . 4
⊢
((℩𝑦
∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵 → ((℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) ∈ 𝐻 ↔ 𝐵 ∈ 𝐻)) |
20 | 18, 19 | syl5ibcom 235 |
. . 3
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ((℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵 → 𝐵 ∈ 𝐻)) |
21 | 20 | pm4.71rd 667 |
. 2
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ((℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵))) |
22 | | shsss 28172 |
. . . . . 6
⊢ ((𝐻 ∈
Sℋ ∧ (⊥‘𝐻) ∈ Sℋ )
→ (𝐻
+ℋ (⊥‘𝐻)) ⊆ ℋ) |
23 | 1, 3, 22 | syl2anc 693 |
. . . . 5
⊢ (𝐻 ∈
Cℋ → (𝐻 +ℋ (⊥‘𝐻)) ⊆
ℋ) |
24 | 23 | sselda 3603 |
. . . 4
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → 𝐴 ∈ ℋ) |
25 | | pjhval 28256 |
. . . 4
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ ℋ) →
((projℎ‘𝐻)‘𝐴) = (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
26 | 24, 25 | syldan 487 |
. . 3
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) →
((projℎ‘𝐻)‘𝐴) = (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥))) |
27 | 26 | eqeq1d 2624 |
. 2
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) →
(((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵)) |
28 | | id 22 |
. . . 4
⊢ (𝐵 ∈ 𝐻 → 𝐵 ∈ 𝐻) |
29 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 +ℎ 𝑥) = (𝐵 +ℎ 𝑥)) |
30 | 29 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 = (𝑦 +ℎ 𝑥) ↔ 𝐴 = (𝐵 +ℎ 𝑥))) |
31 | 30 | rexbidv 3052 |
. . . . 5
⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥) ↔ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥))) |
32 | 31 | riota2 6633 |
. . . 4
⊢ ((𝐵 ∈ 𝐻 ∧ ∃!𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) → (∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥) ↔ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵)) |
33 | 28, 16, 32 | syl2anr 495 |
. . 3
⊢ (((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) ∧ 𝐵 ∈ 𝐻) → (∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥) ↔ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵)) |
34 | 33 | pm5.32da 673 |
. 2
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) → ((𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)) ↔ (𝐵 ∈ 𝐻 ∧ (℩𝑦 ∈ 𝐻 ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝑦 +ℎ 𝑥)) = 𝐵))) |
35 | 21, 27, 34 | 3bitr4d 300 |
1
⊢ ((𝐻 ∈
Cℋ ∧ 𝐴 ∈ (𝐻 +ℋ (⊥‘𝐻))) →
(((projℎ‘𝐻)‘𝐴) = 𝐵 ↔ (𝐵 ∈ 𝐻 ∧ ∃𝑥 ∈ (⊥‘𝐻)𝐴 = (𝐵 +ℎ 𝑥)))) |