Step | Hyp | Ref
| Expression |
1 | | psseq1 4048 |
. . . 4
β’ (π΄ = if(π΄ β Cβ ,
π΄, β) β (π΄ β π΅ β if(π΄ β Cβ ,
π΄, β) β π΅)) |
2 | | oveq1 7365 |
. . . . 5
β’ (π΄ = if(π΄ β Cβ ,
π΄, β) β (π΄ β¨β
(spanβ{πΆ})) =
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ}))) |
3 | 2 | sseq2d 3977 |
. . . 4
β’ (π΄ = if(π΄ β Cβ ,
π΄, β) β (π΅ β (π΄ β¨β (spanβ{πΆ})) β π΅ β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ})))) |
4 | 1, 3 | anbi12d 632 |
. . 3
β’ (π΄ = if(π΄ β Cβ ,
π΄, β) β ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β (if(π΄ β
Cβ , π΄, β) β π΅ β§ π΅ β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))))) |
5 | 2 | eqeq2d 2744 |
. . 3
β’ (π΄ = if(π΄ β Cβ ,
π΄, β) β (π΅ = (π΄ β¨β (spanβ{πΆ})) β π΅ = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ})))) |
6 | 4, 5 | imbi12d 345 |
. 2
β’ (π΄ = if(π΄ β Cβ ,
π΄, β) β (((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β π΅ = (π΄ β¨β (spanβ{πΆ}))) β ((if(π΄ β
Cβ , π΄, β) β π΅ β§ π΅ β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))) β π΅ = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))))) |
7 | | psseq2 4049 |
. . . 4
β’ (π΅ = if(π΅ β Cβ ,
π΅, β) β
(if(π΄ β
Cβ , π΄, β) β π΅ β if(π΄ β Cβ ,
π΄, β) β
if(π΅ β
Cβ , π΅, β))) |
8 | | sseq1 3970 |
. . . 4
β’ (π΅ = if(π΅ β Cβ ,
π΅, β) β (π΅ β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ})) β if(π΅ β Cβ ,
π΅, β) β
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ})))) |
9 | 7, 8 | anbi12d 632 |
. . 3
β’ (π΅ = if(π΅ β Cβ ,
π΅, β) β
((if(π΄ β
Cβ , π΄, β) β π΅ β§ π΅ β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))) β (if(π΄ β Cβ ,
π΄, β) β
if(π΅ β
Cβ , π΅, β) β§ if(π΅ β Cβ ,
π΅, β) β
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ}))))) |
10 | | eqeq1 2737 |
. . 3
β’ (π΅ = if(π΅ β Cβ ,
π΅, β) β (π΅ = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ})) β if(π΅ β Cβ ,
π΅, β) = (if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ})))) |
11 | 9, 10 | imbi12d 345 |
. 2
β’ (π΅ = if(π΅ β Cβ ,
π΅, β) β
(((if(π΄ β
Cβ , π΄, β) β π΅ β§ π΅ β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))) β π΅ = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))) β ((if(π΄ β Cβ ,
π΄, β) β
if(π΅ β
Cβ , π΅, β) β§ if(π΅ β Cβ ,
π΅, β) β
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ}))) β
if(π΅ β
Cβ , π΅, β) = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))))) |
12 | | sneq 4597 |
. . . . . . 7
β’ (πΆ = if(πΆ β β, πΆ, 0β) β {πΆ} = {if(πΆ β β, πΆ, 0β)}) |
13 | 12 | fveq2d 6847 |
. . . . . 6
β’ (πΆ = if(πΆ β β, πΆ, 0β) β
(spanβ{πΆ}) =
(spanβ{if(πΆ β
β, πΆ,
0β)})) |
14 | 13 | oveq2d 7374 |
. . . . 5
β’ (πΆ = if(πΆ β β, πΆ, 0β) β (if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ})) =
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{if(πΆ β
β, πΆ,
0β)}))) |
15 | 14 | sseq2d 3977 |
. . . 4
β’ (πΆ = if(πΆ β β, πΆ, 0β) β (if(π΅ β
Cβ , π΅, β) β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ})) β if(π΅ β Cβ ,
π΅, β) β
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{if(πΆ β
β, πΆ,
0β)})))) |
16 | 15 | anbi2d 630 |
. . 3
β’ (πΆ = if(πΆ β β, πΆ, 0β) β ((if(π΄ β
Cβ , π΄, β) β if(π΅ β Cβ ,
π΅, β) β§ if(π΅ β
Cβ , π΅, β) β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))) β (if(π΄ β Cβ ,
π΄, β) β
if(π΅ β
Cβ , π΅, β) β§ if(π΅ β Cβ ,
π΅, β) β
(if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{if(πΆ β
β, πΆ,
0β)}))))) |
17 | 14 | eqeq2d 2744 |
. . 3
β’ (πΆ = if(πΆ β β, πΆ, 0β) β (if(π΅ β
Cβ , π΅, β) = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ})) β if(π΅ β Cβ ,
π΅, β) = (if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{if(πΆ β
β, πΆ,
0β)})))) |
18 | 16, 17 | imbi12d 345 |
. 2
β’ (πΆ = if(πΆ β β, πΆ, 0β) β (((if(π΄ β
Cβ , π΄, β) β if(π΅ β Cβ ,
π΅, β) β§ if(π΅ β
Cβ , π΅, β) β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{πΆ}))) β if(π΅ β Cβ ,
π΅, β) = (if(π΄ β
Cβ , π΄, β) β¨β
(spanβ{πΆ}))) β
((if(π΄ β
Cβ , π΄, β) β if(π΅ β Cβ ,
π΅, β) β§ if(π΅ β
Cβ , π΅, β) β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{if(πΆ β β, πΆ, 0β)}))) β if(π΅ β
Cβ , π΅, β) = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{if(πΆ β β, πΆ,
0β)}))))) |
19 | | ifchhv 30228 |
. . 3
β’ if(π΄ β
Cβ , π΄, β) β
Cβ |
20 | | ifchhv 30228 |
. . 3
β’ if(π΅ β
Cβ , π΅, β) β
Cβ |
21 | | ifhvhv0 30006 |
. . 3
β’ if(πΆ β β, πΆ, 0β) β
β |
22 | 19, 20, 21 | spansncvi 30636 |
. 2
β’
((if(π΄ β
Cβ , π΄, β) β if(π΅ β Cβ ,
π΅, β) β§ if(π΅ β
Cβ , π΅, β) β (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{if(πΆ β β, πΆ, 0β)}))) β if(π΅ β
Cβ , π΅, β) = (if(π΄ β Cβ ,
π΄, β)
β¨β (spanβ{if(πΆ β β, πΆ, 0β)}))) |
23 | 6, 11, 18, 22 | dedth3h 4547 |
1
β’ ((π΄ β
Cβ β§ π΅ β Cβ
β§ πΆ β β)
β ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β π΅ = (π΄ β¨β (spanβ{πΆ})))) |