Step | Hyp | Ref
| Expression |
1 | | iccssre 13353 |
. . . . . . 7
β’ ((π΅ β β β§ πΆ β β) β (π΅[,]πΆ) β β) |
2 | 1 | adantl 483 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (π΅[,]πΆ) β β) |
3 | | dfss4 4223 |
. . . . . 6
β’ ((π΅[,]πΆ) β β β (β β
(β β (π΅[,]πΆ))) = (π΅[,]πΆ)) |
4 | 2, 3 | sylib 217 |
. . . . 5
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β β
(β β (π΅[,]πΆ))) = (π΅[,]πΆ)) |
5 | | difreicc 13408 |
. . . . . . 7
β’ ((π΅ β β β§ πΆ β β) β (β
β (π΅[,]πΆ)) = ((-β(,)π΅) βͺ (πΆ(,)+β))) |
6 | 5 | adantl 483 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β β
(π΅[,]πΆ)) = ((-β(,)π΅) βͺ (πΆ(,)+β))) |
7 | 6 | difeq2d 4087 |
. . . . 5
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β β
(β β (π΅[,]πΆ))) = (β β
((-β(,)π΅) βͺ
(πΆ(,)+β)))) |
8 | 4, 7 | eqtr3d 2779 |
. . . 4
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (π΅[,]πΆ) = (β β ((-β(,)π΅) βͺ (πΆ(,)+β)))) |
9 | 8 | imaeq2d 6018 |
. . 3
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (π΅[,]πΆ)) = (β‘πΉ β (β β ((-β(,)π΅) βͺ (πΆ(,)+β))))) |
10 | | ffun 6676 |
. . . . . 6
β’ (πΉ:π΄βΆβ β Fun πΉ) |
11 | | funcnvcnv 6573 |
. . . . . 6
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
12 | 10, 11 | syl 17 |
. . . . 5
β’ (πΉ:π΄βΆβ β Fun β‘β‘πΉ) |
13 | 12 | ad2antlr 726 |
. . . 4
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β Fun β‘β‘πΉ) |
14 | | imadif 6590 |
. . . 4
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (β β ((-β(,)π΅) βͺ (πΆ(,)+β)))) = ((β‘πΉ β β) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β))))) |
15 | 13, 14 | syl 17 |
. . 3
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (β β ((-β(,)π΅) βͺ (πΆ(,)+β)))) = ((β‘πΉ β β) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β))))) |
16 | 9, 15 | eqtrd 2777 |
. 2
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (π΅[,]πΆ)) = ((β‘πΉ β β) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β))))) |
17 | | fimacnv 6695 |
. . . . . 6
β’ (πΉ:π΄βΆβ β (β‘πΉ β β) = π΄) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β β) = π΄) |
19 | | mbfdm 25006 |
. . . . . 6
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
20 | | fdm 6682 |
. . . . . . . 8
β’ (πΉ:π΄βΆβ β dom πΉ = π΄) |
21 | 20 | eleq1d 2823 |
. . . . . . 7
β’ (πΉ:π΄βΆβ β (dom πΉ β dom vol β π΄ β dom
vol)) |
22 | 21 | biimpac 480 |
. . . . . 6
β’ ((dom
πΉ β dom vol β§
πΉ:π΄βΆβ) β π΄ β dom vol) |
23 | 19, 22 | sylan 581 |
. . . . 5
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β π΄ β dom vol) |
24 | 18, 23 | eqeltrd 2838 |
. . . 4
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β β) β dom
vol) |
25 | | imaundi 6107 |
. . . . 5
β’ (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β))) = ((β‘πΉ β (-β(,)π΅)) βͺ (β‘πΉ β (πΆ(,)+β))) |
26 | | mbfima 25010 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (-β(,)π΅)) β dom vol) |
27 | | mbfima 25010 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (πΆ(,)+β)) β dom
vol) |
28 | | unmbl 24917 |
. . . . . 6
β’ (((β‘πΉ β (-β(,)π΅)) β dom vol β§ (β‘πΉ β (πΆ(,)+β)) β dom vol) β ((β‘πΉ β (-β(,)π΅)) βͺ (β‘πΉ β (πΆ(,)+β))) β dom
vol) |
29 | 26, 27, 28 | syl2anc 585 |
. . . . 5
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β ((β‘πΉ β (-β(,)π΅)) βͺ (β‘πΉ β (πΆ(,)+β))) β dom
vol) |
30 | 25, 29 | eqeltrid 2842 |
. . . 4
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β))) β dom
vol) |
31 | | difmbl 24923 |
. . . 4
β’ (((β‘πΉ β β) β dom vol β§
(β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β))) β dom vol) β
((β‘πΉ β β) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β)))) β dom
vol) |
32 | 24, 30, 31 | syl2anc 585 |
. . 3
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β ((β‘πΉ β β) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β)))) β dom
vol) |
33 | 32 | adantr 482 |
. 2
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β ((β‘πΉ β β) β (β‘πΉ β ((-β(,)π΅) βͺ (πΆ(,)+β)))) β dom
vol) |
34 | 16, 33 | eqeltrd 2838 |
1
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (π΅[,]πΆ)) β dom vol) |