Step | Hyp | Ref
| Expression |
1 | | spansn 31413 |
. . . 4
β’ (π΅ β β β
(spanβ{π΅}) =
(β₯β(β₯β{π΅}))) |
2 | 1 | eleq2d 2811 |
. . 3
β’ (π΅ β β β (π΄ β (spanβ{π΅}) β π΄ β (β₯β(β₯β{π΅})))) |
3 | 2 | 3ad2ant2 1131 |
. 2
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0β)
β (π΄ β
(spanβ{π΅}) β
π΄ β
(β₯β(β₯β{π΅})))) |
4 | | eleq1 2813 |
. . . . . 6
β’ (π΄ = if(π΄ β β, π΄, 0β) β (π΄ β
(β₯β(β₯β{π΅})) β if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{π΅})))) |
5 | | id 22 |
. . . . . . 7
β’ (π΄ = if(π΄ β β, π΄, 0β) β π΄ = if(π΄ β β, π΄, 0β)) |
6 | | oveq1 7423 |
. . . . . . . . 9
β’ (π΄ = if(π΄ β β, π΄, 0β) β (π΄
Β·ih π΅) = (if(π΄ β β, π΄, 0β)
Β·ih π΅)) |
7 | 6 | oveq1d 7431 |
. . . . . . . 8
β’ (π΄ = if(π΄ β β, π΄, 0β) β ((π΄
Β·ih π΅) / (π΅ Β·ih π΅)) = ((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))) |
8 | 7 | oveq1d 7431 |
. . . . . . 7
β’ (π΄ = if(π΄ β β, π΄, 0β) β (((π΄
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅) = (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅)) |
9 | 5, 8 | eqeq12d 2741 |
. . . . . 6
β’ (π΄ = if(π΄ β β, π΄, 0β) β (π΄ = (((π΄ Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅) β if(π΄ β β, π΄, 0β) = (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅))) |
10 | 4, 9 | bibi12d 344 |
. . . . 5
β’ (π΄ = if(π΄ β β, π΄, 0β) β ((π΄ β
(β₯β(β₯β{π΅})) β π΄ = (((π΄ Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅)) β (if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{π΅})) β if(π΄ β β, π΄, 0β) = (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅)))) |
11 | 10 | imbi2d 339 |
. . . 4
β’ (π΄ = if(π΄ β β, π΄, 0β) β ((π΅ β 0β
β (π΄ β
(β₯β(β₯β{π΅})) β π΄ = (((π΄ Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅))) β (π΅ β 0β β (if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{π΅})) β if(π΄ β β, π΄, 0β) = (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅))))) |
12 | | neeq1 2993 |
. . . . 5
β’ (π΅ = if(π΅ β β, π΅, 0β) β (π΅ β 0β
β if(π΅ β β,
π΅, 0β)
β 0β)) |
13 | | sneq 4634 |
. . . . . . . . 9
β’ (π΅ = if(π΅ β β, π΅, 0β) β {π΅} = {if(π΅ β β, π΅, 0β)}) |
14 | 13 | fveq2d 6896 |
. . . . . . . 8
β’ (π΅ = if(π΅ β β, π΅, 0β) β
(β₯β{π΅}) =
(β₯β{if(π΅ β
β, π΅,
0β)})) |
15 | 14 | fveq2d 6896 |
. . . . . . 7
β’ (π΅ = if(π΅ β β, π΅, 0β) β
(β₯β(β₯β{π΅})) =
(β₯β(β₯β{if(π΅ β β, π΅, 0β)}))) |
16 | 15 | eleq2d 2811 |
. . . . . 6
β’ (π΅ = if(π΅ β β, π΅, 0β) β (if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{π΅})) β if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{if(π΅ β β, π΅,
0β)})))) |
17 | | oveq2 7424 |
. . . . . . . . 9
β’ (π΅ = if(π΅ β β, π΅, 0β) β (if(π΄ β β, π΄, 0β)
Β·ih π΅) = (if(π΄ β β, π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β))) |
18 | | oveq1 7423 |
. . . . . . . . . 10
β’ (π΅ = if(π΅ β β, π΅, 0β) β (π΅
Β·ih π΅) = (if(π΅ β β, π΅, 0β)
Β·ih π΅)) |
19 | | oveq2 7424 |
. . . . . . . . . 10
β’ (π΅ = if(π΅ β β, π΅, 0β) β (if(π΅ β β, π΅, 0β)
Β·ih π΅) = (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β))) |
20 | 18, 19 | eqtrd 2765 |
. . . . . . . . 9
β’ (π΅ = if(π΅ β β, π΅, 0β) β (π΅
Β·ih π΅) = (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β))) |
21 | 17, 20 | oveq12d 7434 |
. . . . . . . 8
β’ (π΅ = if(π΅ β β, π΅, 0β) β ((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅)) = ((if(π΄ β β, π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β)) / (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β)))) |
22 | | id 22 |
. . . . . . . 8
β’ (π΅ = if(π΅ β β, π΅, 0β) β π΅ = if(π΅ β β, π΅, 0β)) |
23 | 21, 22 | oveq12d 7434 |
. . . . . . 7
β’ (π΅ = if(π΅ β β, π΅, 0β) β (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅) = (((if(π΄ β β, π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β)) / (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β)))
Β·β if(π΅ β β, π΅, 0β))) |
24 | 23 | eqeq2d 2736 |
. . . . . 6
β’ (π΅ = if(π΅ β β, π΅, 0β) β (if(π΄ β β, π΄, 0β) =
(((if(π΄ β β,
π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅) β if(π΄ β β, π΄, 0β) = (((if(π΄ β β, π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β)) / (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β)))
Β·β if(π΅ β β, π΅, 0β)))) |
25 | 16, 24 | bibi12d 344 |
. . . . 5
β’ (π΅ = if(π΅ β β, π΅, 0β) β ((if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{π΅})) β if(π΄ β β, π΄, 0β) = (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅)) β (if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{if(π΅ β β, π΅, 0β)})) β if(π΄ β β, π΄, 0β) =
(((if(π΄ β β,
π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β)) / (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β)))
Β·β if(π΅ β β, π΅, 0β))))) |
26 | 12, 25 | imbi12d 343 |
. . . 4
β’ (π΅ = if(π΅ β β, π΅, 0β) β ((π΅ β 0β
β (if(π΄ β
β, π΄,
0β) β (β₯β(β₯β{π΅})) β if(π΄ β β, π΄, 0β) = (((if(π΄ β β, π΄, 0β)
Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅))) β (if(π΅ β β, π΅, 0β) β
0β β (if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{if(π΅ β β, π΅, 0β)})) β if(π΄ β β, π΄, 0β) =
(((if(π΄ β β,
π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β)) / (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β)))
Β·β if(π΅ β β, π΅,
0β)))))) |
27 | | ifhvhv0 30876 |
. . . . 5
β’ if(π΄ β β, π΄, 0β) β
β |
28 | | ifhvhv0 30876 |
. . . . 5
β’ if(π΅ β β, π΅, 0β) β
β |
29 | 27, 28 | h1de2bi 31408 |
. . . 4
β’ (if(π΅ β β, π΅, 0β) β
0β β (if(π΄ β β, π΄, 0β) β
(β₯β(β₯β{if(π΅ β β, π΅, 0β)})) β if(π΄ β β, π΄, 0β) =
(((if(π΄ β β,
π΄, 0β)
Β·ih if(π΅ β β, π΅, 0β)) / (if(π΅ β β, π΅, 0β)
Β·ih if(π΅ β β, π΅, 0β)))
Β·β if(π΅ β β, π΅, 0β)))) |
30 | 11, 26, 29 | dedth2h 4583 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β (π΅ β 0β
β (π΄ β
(β₯β(β₯β{π΅})) β π΄ = (((π΄ Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅)))) |
31 | 30 | 3impia 1114 |
. 2
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0β)
β (π΄ β
(β₯β(β₯β{π΅})) β π΄ = (((π΄ Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅))) |
32 | 3, 31 | bitrd 278 |
1
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0β)
β (π΄ β
(spanβ{π΅}) β
π΄ = (((π΄ Β·ih π΅) / (π΅ Β·ih π΅))
Β·β π΅))) |