Step | Hyp | Ref
| Expression |
1 | | spansnch 30808 |
. . . 4
β’ (π΄ β β β
(spanβ{π΄}) β
Cβ ) |
2 | 1 | 3ad2ant1 1133 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β (spanβ{π΄})
β Cβ ) |
3 | | simp2 1137 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β π΅ β
β) |
4 | | eqid 2732 |
. . . . 5
β’
((projββ(spanβ{π΄}))βπ΅) =
((projββ(spanβ{π΄}))βπ΅) |
5 | | pjeq 30647 |
. . . . 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 496 |
. . 3
β’
(((spanβ{π΄})
β Cβ β§ π΅ β β) β βπ¦ β
(β₯β(spanβ{π΄}))π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦)) |
8 | 2, 3, 7 | syl2anc 584 |
. 2
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β βπ¦ β
(β₯β(spanβ{π΄}))π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦)) |
9 | | oveq1 7415 |
. . . . . . 7
β’ (π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦) β (π΅ Β·ih π΄) =
((((projββ(spanβ{π΄}))βπ΅) +β π¦) Β·ih π΄)) |
10 | 9 | ad2antll 727 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β (π΅ Β·ih π΄) =
((((projββ(spanβ{π΄}))βπ΅) +β π¦) Β·ih π΄)) |
11 | | pjhcl 30649 |
. . . . . . . . . . 11
β’
(((spanβ{π΄})
β Cβ β§ π΅ β β) β
((projββ(spanβ{π΄}))βπ΅) β β) |
12 | 2, 3, 11 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β ((projββ(spanβ{π΄}))βπ΅) β β) |
13 | 12 | adantr 481 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β
((projββ(spanβ{π΄}))βπ΅) β β) |
14 | | choccl 30554 |
. . . . . . . . . . . 12
β’
((spanβ{π΄})
β Cβ β
(β₯β(spanβ{π΄})) β Cβ
) |
15 | 1, 14 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β β β
(β₯β(spanβ{π΄})) β Cβ
) |
16 | 15 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β (β₯β(spanβ{π΄})) β Cβ
) |
17 | | chel 30478 |
. . . . . . . . . 10
β’
(((β₯β(spanβ{π΄})) β Cβ
β§ π¦ β
(β₯β(spanβ{π΄}))) β π¦ β β) |
18 | 16, 17 | sylan 580 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β π¦ β β) |
19 | | simpl1 1191 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β π΄ β β) |
20 | | ax-his2 30331 |
. . . . . . . . 9
β’
((((projββ(spanβ{π΄}))βπ΅) β β β§ π¦ β β β§ π΄ β β) β
((((projββ(spanβ{π΄}))βπ΅) +β π¦) Β·ih π΄) =
((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) + (π¦ Β·ih π΄))) |
21 | 13, 18, 19, 20 | syl3anc 1371 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β
((((projββ(spanβ{π΄}))βπ΅) +β π¦) Β·ih π΄) =
((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) + (π¦ Β·ih π΄))) |
22 | | spansnsh 30809 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
(spanβ{π΄}) β
Sβ ) |
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β (spanβ{π΄}) β Sβ
) |
24 | | spansnid 30811 |
. . . . . . . . . . . . 13
β’ (π΄ β β β π΄ β (spanβ{π΄})) |
25 | 24 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β π΄ β (spanβ{π΄})) |
26 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β π¦ β (β₯β(spanβ{π΄}))) |
27 | | shocorth 30540 |
. . . . . . . . . . . . 13
β’
((spanβ{π΄})
β Sβ β ((π΄ β (spanβ{π΄}) β§ π¦ β (β₯β(spanβ{π΄}))) β (π΄ Β·ih π¦) = 0)) |
28 | 27 | 3impib 1116 |
. . . . . . . . . . . 12
β’
(((spanβ{π΄})
β Sβ β§ π΄ β (spanβ{π΄}) β§ π¦ β (β₯β(spanβ{π΄}))) β (π΄ Β·ih π¦) = 0) |
29 | 23, 25, 26, 28 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β (π΄ Β·ih π¦) = 0) |
30 | 15, 17 | sylan 580 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β π¦ β β) |
31 | | orthcom 30356 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β β) β ((π΄
Β·ih π¦) = 0 β (π¦ Β·ih π΄) = 0)) |
32 | 30, 31 | syldan 591 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β ((π΄ Β·ih π¦) = 0 β (π¦ Β·ih π΄) = 0)) |
33 | 29, 32 | mpbid 231 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β
(β₯β(spanβ{π΄}))) β (π¦ Β·ih π΄) = 0) |
34 | 33 | 3ad2antl1 1185 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β (π¦ Β·ih π΄) = 0) |
35 | 34 | oveq2d 7424 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β
((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) + (π¦ Β·ih π΄)) =
((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) + 0)) |
36 | | hicl 30328 |
. . . . . . . . . 10
β’
((((projββ(spanβ{π΄}))βπ΅) β β β§ π΄ β β) β
(((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) β
β) |
37 | 13, 19, 36 | syl2anc 584 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β
(((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) β
β) |
38 | 37 | addridd 11413 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β
((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) + 0) =
(((projββ(spanβ{π΄}))βπ΅) Β·ih π΄)) |
39 | 21, 35, 38 | 3eqtrd 2776 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ π¦ β
(β₯β(spanβ{π΄}))) β
((((projββ(spanβ{π΄}))βπ΅) +β π¦) Β·ih π΄) =
(((projββ(spanβ{π΄}))βπ΅) Β·ih π΄)) |
40 | 39 | adantrr 715 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β
((((projββ(spanβ{π΄}))βπ΅) +β π¦) Β·ih π΄) =
(((projββ(spanβ{π΄}))βπ΅) Β·ih π΄)) |
41 | 10, 40 | eqtrd 2772 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β (π΅ Β·ih π΄) =
(((projββ(spanβ{π΄}))βπ΅) Β·ih π΄)) |
42 | 41 | oveq1d 7423 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β ((π΅ Β·ih π΄) /
((normββπ΄)β2)) =
((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) /
((normββπ΄)β2))) |
43 | 42 | oveq1d 7423 |
. . 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 30648 |
. . . . . 6
β’
(((spanβ{π΄})
β Cβ β§ π΅ β β) β
((projββ(spanβ{π΄}))βπ΅) β (spanβ{π΄})) |
47 | 2, 3, 46 | syl2anc 584 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β ((projββ(spanβ{π΄}))βπ΅) β (spanβ{π΄})) |
48 | 47 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β
((projββ(spanβ{π΄}))βπ΅) β (spanβ{π΄})) |
49 | | normcan 30824 |
. . . 4
β’ ((π΄ β β β§ π΄ β 0β β§
((projββ(spanβ{π΄}))βπ΅) β (spanβ{π΄})) β
(((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) /
((normββπ΄)β2))
Β·β π΄) =
((projββ(spanβ{π΄}))βπ΅)) |
50 | 44, 45, 48, 49 | syl3anc 1371 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β
(((((projββ(spanβ{π΄}))βπ΅) Β·ih π΄) /
((normββπ΄)β2))
Β·β π΄) =
((projββ(spanβ{π΄}))βπ΅)) |
51 | 43, 50 | eqtr2d 2773 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β§ (π¦ β
(β₯β(spanβ{π΄})) β§ π΅ =
(((projββ(spanβ{π΄}))βπ΅) +β π¦))) β
((projββ(spanβ{π΄}))βπ΅) = (((π΅ Β·ih π΄) /
((normββπ΄)β2))
Β·β π΄)) |
52 | 8, 51 | rexlimddv 3161 |
1
β’ ((π΄ β β β§ π΅ β β β§ π΄ β 0β)
β ((projββ(spanβ{π΄}))βπ΅) = (((π΅ Β·ih π΄) /
((normββπ΄)β2))
Β·β π΄)) |