Proof of Theorem pjssmii
Step | Hyp | Ref
| Expression |
1 | | pjsslem.1 |
. . . . 5
⊢ 𝐺 ∈
Cℋ |
2 | | pjidm.1 |
. . . . . 6
⊢ 𝐻 ∈
Cℋ |
3 | 2 | choccli 28166 |
. . . . 5
⊢
(⊥‘𝐻)
∈ Cℋ |
4 | 1, 3 | chincli 28319 |
. . . 4
⊢ (𝐺 ∩ (⊥‘𝐻)) ∈
Cℋ |
5 | | pjidm.2 |
. . . . 5
⊢ 𝐴 ∈ ℋ |
6 | 1, 5 | pjhclii 28281 |
. . . 4
⊢
((projℎ‘𝐺)‘𝐴) ∈ ℋ |
7 | 2, 5 | pjhclii 28281 |
. . . 4
⊢
((projℎ‘𝐻)‘𝐴) ∈ ℋ |
8 | 4, 6, 7 | pjsubii 28537 |
. . 3
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) = (((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) −ℎ
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴))) |
9 | 4, 6 | pjhclii 28281 |
. . . . 5
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) ∈ ℋ |
10 | 4, 7 | pjhclii 28281 |
. . . . 5
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴)) ∈ ℋ |
11 | 9, 10 | hvsubvali 27877 |
. . . 4
⊢
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) −ℎ
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴))) = (((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) +ℎ (-1
·ℎ ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴)))) |
12 | | inss1 3833 |
. . . . . . 7
⊢ (𝐺 ∩ (⊥‘𝐻)) ⊆ 𝐺 |
13 | 4, 5, 1 | pjss2i 28539 |
. . . . . . 7
⊢ ((𝐺 ∩ (⊥‘𝐻)) ⊆ 𝐺 →
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴)) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) |
15 | 2 | chshii 28084 |
. . . . . . . . . . . 12
⊢ 𝐻 ∈
Sℋ |
16 | | shococss 28153 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈
Sℋ → 𝐻 ⊆ (⊥‘(⊥‘𝐻))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝐻 ⊆
(⊥‘(⊥‘𝐻)) |
18 | | inss2 3834 |
. . . . . . . . . . . 12
⊢ (𝐺 ∩ (⊥‘𝐻)) ⊆ (⊥‘𝐻) |
19 | 4, 3 | chsscon3i 28320 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∩ (⊥‘𝐻)) ⊆ (⊥‘𝐻) ↔
(⊥‘(⊥‘𝐻)) ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻)))) |
20 | 18, 19 | mpbi 220 |
. . . . . . . . . . 11
⊢
(⊥‘(⊥‘𝐻)) ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
21 | 17, 20 | sstri 3612 |
. . . . . . . . . 10
⊢ 𝐻 ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
22 | 2, 5 | pjclii 28280 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻)‘𝐴) ∈ 𝐻 |
23 | 21, 22 | sselii 3600 |
. . . . . . . . 9
⊢
((projℎ‘𝐻)‘𝐴) ∈ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
24 | 4, 7 | pjoc2i 28297 |
. . . . . . . . 9
⊢
(((projℎ‘𝐻)‘𝐴) ∈ (⊥‘(𝐺 ∩ (⊥‘𝐻))) ↔
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴)) = 0ℎ) |
25 | 23, 24 | mpbi 220 |
. . . . . . . 8
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴)) = 0ℎ |
26 | 25 | oveq2i 6661 |
. . . . . . 7
⊢ (-1
·ℎ ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴))) = (-1 ·ℎ
0ℎ) |
27 | | neg1cn 11124 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
28 | | hvmul0 27881 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1 ·ℎ
0ℎ) = 0ℎ) |
29 | 27, 28 | ax-mp 5 |
. . . . . . 7
⊢ (-1
·ℎ 0ℎ) =
0ℎ |
30 | 26, 29 | eqtri 2644 |
. . . . . 6
⊢ (-1
·ℎ ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴))) = 0ℎ |
31 | 14, 30 | oveq12i 6662 |
. . . . 5
⊢
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) +ℎ (-1
·ℎ ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴)))) = (((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) +ℎ
0ℎ) |
32 | 4, 5 | pjhclii 28281 |
. . . . . 6
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) ∈ ℋ |
33 | | ax-hvaddid 27861 |
. . . . . 6
⊢
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) ∈ ℋ →
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) +ℎ 0ℎ)
= ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴)) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
⊢
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) +ℎ 0ℎ)
= ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) |
35 | 31, 34 | eqtri 2644 |
. . . 4
⊢
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) +ℎ (-1
·ℎ ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴)))) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) |
36 | 11, 35 | eqtri 2644 |
. . 3
⊢
(((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐺)‘𝐴)) −ℎ
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘((projℎ‘𝐻)‘𝐴))) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) |
37 | 8, 36 | eqtri 2644 |
. 2
⊢
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) |
38 | 1, 5 | pjclii 28280 |
. . . . 5
⊢
((projℎ‘𝐺)‘𝐴) ∈ 𝐺 |
39 | | ssel 3597 |
. . . . . 6
⊢ (𝐻 ⊆ 𝐺 →
(((projℎ‘𝐻)‘𝐴) ∈ 𝐻 →
((projℎ‘𝐻)‘𝐴) ∈ 𝐺)) |
40 | 22, 39 | mpi 20 |
. . . . 5
⊢ (𝐻 ⊆ 𝐺 →
((projℎ‘𝐻)‘𝐴) ∈ 𝐺) |
41 | 1 | chshii 28084 |
. . . . . 6
⊢ 𝐺 ∈
Sℋ |
42 | | shsubcl 28077 |
. . . . . 6
⊢ ((𝐺 ∈
Sℋ ∧ ((projℎ‘𝐺)‘𝐴) ∈ 𝐺 ∧ ((projℎ‘𝐻)‘𝐴) ∈ 𝐺) →
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ 𝐺) |
43 | 41, 42 | mp3an1 1411 |
. . . . 5
⊢
((((projℎ‘𝐺)‘𝐴) ∈ 𝐺 ∧ ((projℎ‘𝐻)‘𝐴) ∈ 𝐺) →
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ 𝐺) |
44 | 38, 40, 43 | sylancr 695 |
. . . 4
⊢ (𝐻 ⊆ 𝐺 →
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ 𝐺) |
45 | 2, 5, 1 | pjsslem 28538 |
. . . . 5
⊢
(((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ
((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) |
46 | 2, 1 | chsscon3i 28320 |
. . . . . 6
⊢ (𝐻 ⊆ 𝐺 ↔ (⊥‘𝐺) ⊆ (⊥‘𝐻)) |
47 | 3, 5 | pjclii 28280 |
. . . . . . 7
⊢
((projℎ‘(⊥‘𝐻))‘𝐴) ∈ (⊥‘𝐻) |
48 | 1 | choccli 28166 |
. . . . . . . . 9
⊢
(⊥‘𝐺)
∈ Cℋ |
49 | 48, 5 | pjclii 28280 |
. . . . . . . 8
⊢
((projℎ‘(⊥‘𝐺))‘𝐴) ∈ (⊥‘𝐺) |
50 | | ssel 3597 |
. . . . . . . 8
⊢
((⊥‘𝐺)
⊆ (⊥‘𝐻)
→ (((projℎ‘(⊥‘𝐺))‘𝐴) ∈ (⊥‘𝐺) →
((projℎ‘(⊥‘𝐺))‘𝐴) ∈ (⊥‘𝐻))) |
51 | 49, 50 | mpi 20 |
. . . . . . 7
⊢
((⊥‘𝐺)
⊆ (⊥‘𝐻)
→ ((projℎ‘(⊥‘𝐺))‘𝐴) ∈ (⊥‘𝐻)) |
52 | 3 | chshii 28084 |
. . . . . . . 8
⊢
(⊥‘𝐻)
∈ Sℋ |
53 | | shsubcl 28077 |
. . . . . . . 8
⊢
(((⊥‘𝐻)
∈ Sℋ ∧
((projℎ‘(⊥‘𝐻))‘𝐴) ∈ (⊥‘𝐻) ∧
((projℎ‘(⊥‘𝐺))‘𝐴) ∈ (⊥‘𝐻)) →
(((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ
((projℎ‘(⊥‘𝐺))‘𝐴)) ∈ (⊥‘𝐻)) |
54 | 52, 53 | mp3an1 1411 |
. . . . . . 7
⊢
((((projℎ‘(⊥‘𝐻))‘𝐴) ∈ (⊥‘𝐻) ∧
((projℎ‘(⊥‘𝐺))‘𝐴) ∈ (⊥‘𝐻)) →
(((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ
((projℎ‘(⊥‘𝐺))‘𝐴)) ∈ (⊥‘𝐻)) |
55 | 47, 51, 54 | sylancr 695 |
. . . . . 6
⊢
((⊥‘𝐺)
⊆ (⊥‘𝐻)
→ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ
((projℎ‘(⊥‘𝐺))‘𝐴)) ∈ (⊥‘𝐻)) |
56 | 46, 55 | sylbi 207 |
. . . . 5
⊢ (𝐻 ⊆ 𝐺 →
(((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ
((projℎ‘(⊥‘𝐺))‘𝐴)) ∈ (⊥‘𝐻)) |
57 | 45, 56 | syl5eqelr 2706 |
. . . 4
⊢ (𝐻 ⊆ 𝐺 →
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ (⊥‘𝐻)) |
58 | 44, 57 | jca 554 |
. . 3
⊢ (𝐻 ⊆ 𝐺 →
((((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ 𝐺 ∧
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ (⊥‘𝐻))) |
59 | | elin 3796 |
. . . 4
⊢
((((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ (𝐺 ∩ (⊥‘𝐻)) ↔
((((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ 𝐺 ∧
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ (⊥‘𝐻))) |
60 | 6, 7 | hvsubcli 27878 |
. . . . 5
⊢
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ ℋ |
61 | 4, 60 | pjchi 28291 |
. . . 4
⊢
((((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ (𝐺 ∩ (⊥‘𝐻)) ↔
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) = (((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) |
62 | 59, 61 | bitr3i 266 |
. . 3
⊢
(((((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ 𝐺 ∧
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) ∈ (⊥‘𝐻)) ↔
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) = (((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) |
63 | 58, 62 | sylib 208 |
. 2
⊢ (𝐻 ⊆ 𝐺 →
((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) = (((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴))) |
64 | 37, 63 | syl5reqr 2671 |
1
⊢ (𝐻 ⊆ 𝐺 →
(((projℎ‘𝐺)‘𝐴) −ℎ
((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴)) |