Step | Hyp | Ref
| Expression |
1 | | dipdir.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
2 | | fveq2 6892 |
. . . . . . 7
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (BaseSetβπ) = (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©))) |
3 | 1, 2 | eqtrid 2785 |
. . . . . 6
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β π
= (BaseSetβif(π
β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))) |
4 | 3 | eleq2d 2820 |
. . . . 5
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (π΄ β π β π΄ β (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)))) |
5 | 3 | eleq2d 2820 |
. . . . 5
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (π΅ β π β π΅ β (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)))) |
6 | 3 | eleq2d 2820 |
. . . . 5
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (πΆ β π β πΆ β (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)))) |
7 | 4, 5, 6 | 3anbi123d 1437 |
. . . 4
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΄ β (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) β§ π΅
β (BaseSetβif(π
β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©)) β§ πΆ β
(BaseSetβif(π β
CPreHilOLD, π,
β¨β¨ + , Β· β©, absβ©))))) |
8 | | dipdir.2 |
. . . . . . . . 9
β’ πΊ = ( +π£
βπ) |
9 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β ( +π£ βπ) = ( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))) |
10 | 8, 9 | eqtrid 2785 |
. . . . . . . 8
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β πΊ
= ( +π£ βif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©))) |
11 | 10 | oveqd 7426 |
. . . . . . 7
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (π΄πΊπ΅) = (π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)) |
12 | 11 | oveq1d 7424 |
. . . . . 6
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β ((π΄πΊπ΅)ππΆ) = ((π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)ππΆ)) |
13 | | dipdir.7 |
. . . . . . . 8
β’ π =
(Β·πOLDβπ) |
14 | | fveq2 6892 |
. . . . . . . 8
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (Β·πOLDβπ) =
(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©))) |
15 | 13, 14 | eqtrid 2785 |
. . . . . . 7
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β π
= (Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©))) |
16 | 15 | oveqd 7426 |
. . . . . 6
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β ((π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)ππΆ) = ((π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ)) |
17 | 12, 16 | eqtrd 2773 |
. . . . 5
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β ((π΄πΊπ΅)ππΆ) = ((π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ)) |
18 | 15 | oveqd 7426 |
. . . . . 6
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (π΄ππΆ) = (π΄(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ)) |
19 | 15 | oveqd 7426 |
. . . . . 6
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (π΅ππΆ) = (π΅(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ)) |
20 | 18, 19 | oveq12d 7427 |
. . . . 5
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β ((π΄ππΆ) + (π΅ππΆ)) = ((π΄(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) + (π΅(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ))) |
21 | 17, 20 | eqeq12d 2749 |
. . . 4
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)) β ((π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) = ((π΄(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) + (π΅(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ)))) |
22 | 7, 21 | imbi12d 345 |
. . 3
β’ (π = if(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©) β (((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) β ((π΄ β (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) β§ π΅
β (BaseSetβif(π
β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©)) β§ πΆ β
(BaseSetβif(π β
CPreHilOLD, π,
β¨β¨ + , Β· β©, absβ©))) β ((π΄( +π£ βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©))π΅)(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) = ((π΄(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) + (π΅(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ))))) |
23 | | eqid 2733 |
. . . 4
β’
(BaseSetβif(π
β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©)) = (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) |
24 | | eqid 2733 |
. . . 4
β’ (
+π£ βif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) = ( +π£ βif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) |
25 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) = ( Β·π OLD βif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©)) |
26 | | eqid 2733 |
. . . 4
β’
(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) = (Β·πOLDβif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©)) |
27 | | elimphu 30074 |
. . . 4
β’ if(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©) β CPreHilOLD |
28 | 23, 24, 25, 26, 27 | ipdiri 30083 |
. . 3
β’ ((π΄ β (BaseSetβif(π β CPreHilOLD,
π, β¨β¨ + ,
Β· β©, absβ©)) β§ π΅ β (BaseSetβif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©)) β§ πΆ
β (BaseSetβif(π
β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))) β ((π΄(
+π£ βif(π β CPreHilOLD, π, β¨β¨ + , Β·
β©, absβ©))π΅)(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) = ((π΄(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ) + (π΅(Β·πOLDβif(π β CPreHilOLD, π, β¨β¨ + , Β· β©,
absβ©))πΆ))) |
29 | 22, 28 | dedth 4587 |
. 2
β’ (π β CPreHilOLD
β ((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)))) |
30 | 29 | imp 408 |
1
β’ ((π β CPreHilOLD
β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) |