| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | spansnch 31580 | . . . 4
⊢ (𝐴 ∈ ℋ →
(span‘{𝐴}) ∈
Cℋ ) | 
| 2 | 1 | 3ad2ant1 1133 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (span‘{𝐴})
∈ Cℋ ) | 
| 3 |  | simp2 1137 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 𝐵 ∈
ℋ) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
((projℎ‘(span‘{𝐴}))‘𝐵) =
((projℎ‘(span‘{𝐴}))‘𝐵) | 
| 5 |  | pjeq 31419 | . . . . 5
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
(((projℎ‘(span‘{𝐴}))‘𝐵) =
((projℎ‘(span‘{𝐴}))‘𝐵) ↔
(((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴}) ∧ ∃𝑦 ∈ (⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦)))) | 
| 6 | 4, 5 | mpbii 233 | . . . 4
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
(((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴}) ∧ ∃𝑦 ∈ (⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) | 
| 7 | 6 | simprd 495 | . . 3
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) → ∃𝑦 ∈
(⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦)) | 
| 8 | 2, 3, 7 | syl2anc 584 | . 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ∃𝑦 ∈
(⊥‘(span‘{𝐴}))𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦)) | 
| 9 |  | oveq1 7439 | . . . . . . 7
⊢ (𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) → (𝐵 ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴)) | 
| 10 | 9 | ad2antll 729 | . . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → (𝐵 ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴)) | 
| 11 |  | pjhcl 31421 | . . . . . . . . . . 11
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ) | 
| 12 | 2, 3, 11 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ) | 
| 13 | 12 | adantr 480 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ) | 
| 14 |  | choccl 31326 | . . . . . . . . . . . 12
⊢
((span‘{𝐴})
∈ Cℋ →
(⊥‘(span‘{𝐴})) ∈ Cℋ
) | 
| 15 | 1, 14 | syl 17 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℋ →
(⊥‘(span‘{𝐴})) ∈ Cℋ
) | 
| 16 | 15 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (⊥‘(span‘{𝐴})) ∈ Cℋ
) | 
| 17 |  | chel 31250 | . . . . . . . . . 10
⊢
(((⊥‘(span‘{𝐴})) ∈ Cℋ
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ ℋ) | 
| 18 | 16, 17 | sylan 580 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ ℋ) | 
| 19 |  | simpl1 1191 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝐴 ∈ ℋ) | 
| 20 |  | ax-his2 31103 | . . . . . . . . 9
⊢
((((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝐴 ∈ ℋ) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + (𝑦 ·ih 𝐴))) | 
| 21 | 13, 18, 19, 20 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + (𝑦 ·ih 𝐴))) | 
| 22 |  | spansnsh 31581 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℋ →
(span‘{𝐴}) ∈
Sℋ ) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (span‘{𝐴}) ∈ Sℋ
) | 
| 24 |  | spansnid 31583 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴})) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝐴 ∈ (span‘{𝐴})) | 
| 26 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ (⊥‘(span‘{𝐴}))) | 
| 27 |  | shocorth 31312 | . . . . . . . . . . . . 13
⊢
((span‘{𝐴})
∈ Sℋ → ((𝐴 ∈ (span‘{𝐴}) ∧ 𝑦 ∈ (⊥‘(span‘{𝐴}))) → (𝐴 ·ih 𝑦) = 0)) | 
| 28 | 27 | 3impib 1116 | . . . . . . . . . . . 12
⊢
(((span‘{𝐴})
∈ Sℋ ∧ 𝐴 ∈ (span‘{𝐴}) ∧ 𝑦 ∈ (⊥‘(span‘{𝐴}))) → (𝐴 ·ih 𝑦) = 0) | 
| 29 | 23, 25, 26, 28 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (𝐴 ·ih 𝑦) = 0) | 
| 30 | 15, 17 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → 𝑦 ∈ ℋ) | 
| 31 |  | orthcom 31128 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝐴
·ih 𝑦) = 0 ↔ (𝑦 ·ih 𝐴) = 0)) | 
| 32 | 30, 31 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → ((𝐴 ·ih 𝑦) = 0 ↔ (𝑦 ·ih 𝐴) = 0)) | 
| 33 | 29, 32 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℋ ∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (𝑦 ·ih 𝐴) = 0) | 
| 34 | 33 | 3ad2antl1 1185 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) → (𝑦 ·ih 𝐴) = 0) | 
| 35 | 34 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + (𝑦 ·ih 𝐴)) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + 0)) | 
| 36 |  | hicl 31100 | . . . . . . . . . 10
⊢
((((projℎ‘(span‘{𝐴}))‘𝐵) ∈ ℋ ∧ 𝐴 ∈ ℋ) →
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) ∈
ℂ) | 
| 37 | 13, 19, 36 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) ∈
ℂ) | 
| 38 | 37 | addridd 11462 | . . . . . . . 8
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) + 0) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) | 
| 39 | 21, 35, 38 | 3eqtrd 2780 | . . . . . . 7
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ 𝑦 ∈
(⊥‘(span‘{𝐴}))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) | 
| 40 | 39 | adantrr 717 | . . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
((((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦) ·ih 𝐴) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) | 
| 41 | 10, 40 | eqtrd 2776 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → (𝐵 ·ih 𝐴) =
(((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴)) | 
| 42 | 41 | oveq1d 7447 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → ((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2)) =
((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))) | 
| 43 | 42 | oveq1d 7447 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → (((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴) =
(((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴)) | 
| 44 |  | simpl1 1191 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → 𝐴 ∈ ℋ) | 
| 45 |  | simpl3 1193 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) → 𝐴 ≠ 0ℎ) | 
| 46 |  | axpjcl 31420 | . . . . . 6
⊢
(((span‘{𝐴})
∈ Cℋ ∧ 𝐵 ∈ ℋ) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) | 
| 47 | 2, 3, 46 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) | 
| 48 | 47 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) | 
| 49 |  | normcan 31596 | . . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ∧
((projℎ‘(span‘{𝐴}))‘𝐵) ∈ (span‘{𝐴})) →
(((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴) =
((projℎ‘(span‘{𝐴}))‘𝐵)) | 
| 50 | 44, 45, 48, 49 | syl3anc 1372 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
(((((projℎ‘(span‘{𝐴}))‘𝐵) ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴) =
((projℎ‘(span‘{𝐴}))‘𝐵)) | 
| 51 | 43, 50 | eqtr2d 2777 | . 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
∧ (𝑦 ∈
(⊥‘(span‘{𝐴})) ∧ 𝐵 =
(((projℎ‘(span‘{𝐴}))‘𝐵) +ℎ 𝑦))) →
((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴)) | 
| 52 | 8, 51 | rexlimddv 3160 | 1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) /
((normℎ‘𝐴)↑2))
·ℎ 𝐴)) |