Step | Hyp | Ref
| Expression |
1 | | spansnch 29901 |
. . . 4
⊢ (𝐴 ∈ ℋ →
(span‘{𝐴}) ∈
Cℋ ) |
2 | 1 | 3ad2ant1 1131 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (span‘{𝐴})
∈ Cℋ ) |
3 | | simp2 1135 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 𝐵 ∈
ℋ) |
4 | | eqid 2739 |
. . . . 5
⊢
((projℎ‘(span‘{𝐴}))‘𝐵) =
((projℎ‘(span‘{𝐴}))‘𝐵) |
5 | | pjeq 29740 |
. . . . 5
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
(((projℎ‘(span‘{𝐴}))‘𝐵) =
((projℎ‘(span‘{𝐴}))‘𝐵) ↔
(((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴}) ∧ ∃𝑦 ∈ (⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦)))) |
6 | 4, 5 | mpbii 232 |
. . . 4
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
(((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴}) ∧ ∃𝑦 ∈ (⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) |
7 | 6 | simprd 495 |
. . 3
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) → ∃𝑦 ∈
(⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦)) |
8 | 2, 3, 7 | syl2anc 583 |
. 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ∃𝑦 ∈
(⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦)) |
9 | | oveq1 7275 |
. . . . . . 7
⊢ (𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) → (𝐵 ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴)) |
10 | 9 | ad2antll 725 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → (𝐵 ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴)) |
11 | | pjhcl 29742 |
. . . . . . . . . . 11
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ) |
12 | 2, 3, 11 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ) |
13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ) |
14 | | choccl 29647 |
. . . . . . . . . . . 12
⊢
((span‘{𝐴})
∈ Cℋ →
(⊥‘(span‘{𝐴})) ∈ Cℋ
) |
15 | 1, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℋ →
(⊥‘(span‘{𝐴})) ∈ Cℋ
) |
16 | 15 | 3ad2ant1 1131 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (⊥‘(span‘{𝐴})) ∈ Cℋ
) |
17 | | chel 29571 |
. . . . . . . . . 10
⊢
(((⊥‘(span‘{𝐴})) ∈ Cℋ
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ ℋ) |
18 | 16, 17 | sylan 579 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ ℋ) |
19 | | simpl1 1189 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝐴 ∈ ℋ) |
20 | | ax-his2 29424 |
. . . . . . . . 9
⊢
((((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝐴 ∈ ℋ) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + (𝑦 ·ih 𝐴))) |
21 | 13, 18, 19, 20 | syl3anc 1369 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + (𝑦 ·ih 𝐴))) |
22 | | spansnsh 29902 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℋ →
(span‘{𝐴}) ∈
Sℋ ) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (span‘{𝐴}) ∈ Sℋ
) |
24 | | spansnid 29904 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴})) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝐴 ∈ (span‘{𝐴})) |
26 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ (⊥‘(span‘{𝐴}))) |
27 | | shocorth 29633 |
. . . . . . . . . . . . 13
⊢
((span‘{𝐴})
∈ Sℋ → ((𝐴 ∈ (span‘{𝐴}) ∧ 𝑦 ∈ (⊥‘(span‘{𝐴}))) → (𝐴 ·ih 𝑦) = 0)) |
28 | 27 | 3impib 1114 |
. . . . . . . . . . . 12
⊢
(((span‘{𝐴})
∈ Sℋ ∧ 𝐴 ∈ (span‘{𝐴}) ∧ 𝑦 ∈ (⊥‘(span‘{𝐴}))) → (𝐴 ·ih 𝑦) = 0) |
29 | 23, 25, 26, 28 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (𝐴 ·ih 𝑦) = 0) |
30 | 15, 17 | sylan 579 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ ℋ) |
31 | | orthcom 29449 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝐴
·ih 𝑦) = 0 ↔ (𝑦 ·ih 𝐴) = 0)) |
32 | 30, 31 | syldan 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → ((𝐴 ·ih 𝑦) = 0 ↔ (𝑦 ·ih 𝐴) = 0)) |
33 | 29, 32 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (𝑦 ·ih 𝐴) = 0) |
34 | 33 | 3ad2antl1 1183 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (𝑦 ·ih 𝐴) = 0) |
35 | 34 | oveq2d 7284 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + (𝑦 ·ih 𝐴)) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + 0)) |
36 | | hicl 29421 |
. . . . . . . . . 10
⊢
((((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ ∧ 𝐴 ∈ ℋ) →
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) ∈
ℂ) |
37 | 13, 19, 36 | syl2anc 583 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) ∈
ℂ) |
38 | 37 | addid1d 11158 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + 0) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) |
39 | 21, 35, 38 | 3eqtrd 2783 |
. . . . . . 7
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) |
40 | 39 | adantrr 713 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) |
41 | 10, 40 | eqtrd 2779 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → (𝐵 ·ih 𝐴) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) |
42 | 41 | oveq1d 7283 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → ((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2)) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))) |
43 | 42 | oveq1d 7283 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → (((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴) =
(((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴)) |
44 | | simpl1 1189 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → 𝐴 ∈ ℋ) |
45 | | simpl3 1191 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → 𝐴 ≠ 0ℎ) |
46 | | axpjcl 29741 |
. . . . . 6
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) |
47 | 2, 3, 46 | syl2anc 583 |
. . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) |
48 | 47 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) |
49 | | normcan 29917 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) →
(((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴) =
((projℎ‘(span‘{𝐴}))‘𝐵)) |
50 | 44, 45, 48, 49 | syl3anc 1369 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
(((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴) =
((projℎ‘(span‘{𝐴}))‘𝐵)) |
51 | 43, 50 | eqtr2d 2780 |
. 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴)) |
52 | 8, 51 | rexlimddv 3221 |
1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴)) |