Step | Hyp | Ref
| Expression |
1 | | stoweidlem2.1 |
. . 3
β’
β²π‘π |
2 | | simpr 486 |
. . . . . 6
β’ ((π β§ π‘ β π) β π‘ β π) |
3 | | stoweidlem2.5 |
. . . . . . 7
β’ (π β πΈ β β) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β πΈ β β) |
5 | | eqidd 2734 |
. . . . . . . 8
β’ (π = π‘ β πΈ = πΈ) |
6 | 5 | cbvmptv 5222 |
. . . . . . 7
β’ (π β π β¦ πΈ) = (π‘ β π β¦ πΈ) |
7 | 6 | fvmpt2 6963 |
. . . . . 6
β’ ((π‘ β π β§ πΈ β β) β ((π β π β¦ πΈ)βπ‘) = πΈ) |
8 | 2, 4, 7 | syl2anc 585 |
. . . . 5
β’ ((π β§ π‘ β π) β ((π β π β¦ πΈ)βπ‘) = πΈ) |
9 | 8 | eqcomd 2739 |
. . . 4
β’ ((π β§ π‘ β π) β πΈ = ((π β π β¦ πΈ)βπ‘)) |
10 | 9 | oveq1d 7376 |
. . 3
β’ ((π β§ π‘ β π) β (πΈ Β· (πΉβπ‘)) = (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘))) |
11 | 1, 10 | mpteq2da 5207 |
. 2
β’ (π β (π‘ β π β¦ (πΈ Β· (πΉβπ‘))) = (π‘ β π β¦ (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘)))) |
12 | | id 22 |
. . . . . . . . 9
β’ (π₯ = πΈ β π₯ = πΈ) |
13 | 12 | mpteq2dv 5211 |
. . . . . . . 8
β’ (π₯ = πΈ β (π‘ β π β¦ π₯) = (π‘ β π β¦ πΈ)) |
14 | 13 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = πΈ β ((π‘ β π β¦ π₯) β π΄ β (π‘ β π β¦ πΈ) β π΄)) |
15 | 14 | imbi2d 341 |
. . . . . 6
β’ (π₯ = πΈ β ((π β (π‘ β π β¦ π₯) β π΄) β (π β (π‘ β π β¦ πΈ) β π΄))) |
16 | | stoweidlem2.3 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
17 | 16 | expcom 415 |
. . . . . 6
β’ (π₯ β β β (π β (π‘ β π β¦ π₯) β π΄)) |
18 | 15, 17 | vtoclga 3536 |
. . . . 5
β’ (πΈ β β β (π β (π‘ β π β¦ πΈ) β π΄)) |
19 | 3, 18 | mpcom 38 |
. . . 4
β’ (π β (π‘ β π β¦ πΈ) β π΄) |
20 | 6, 19 | eqeltrid 2838 |
. . 3
β’ (π β (π β π β¦ πΈ) β π΄) |
21 | | fveq1 6845 |
. . . . . . . 8
β’ (π = (π β π β¦ πΈ) β (πβπ‘) = ((π β π β¦ πΈ)βπ‘)) |
22 | 21 | oveq1d 7376 |
. . . . . . 7
β’ (π = (π β π β¦ πΈ) β ((πβπ‘) Β· (πΉβπ‘)) = (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘))) |
23 | 22 | mpteq2dv 5211 |
. . . . . 6
β’ (π = (π β π β¦ πΈ) β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) = (π‘ β π β¦ (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘)))) |
24 | 23 | eleq1d 2819 |
. . . . 5
β’ (π = (π β π β¦ πΈ) β ((π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄ β (π‘ β π β¦ (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘))) β π΄)) |
25 | 24 | imbi2d 341 |
. . . 4
β’ (π = (π β π β¦ πΈ) β ((π β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄) β (π β (π‘ β π β¦ (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘))) β π΄))) |
26 | | stoweidlem2.6 |
. . . . . . 7
β’ (π β πΉ β π΄) |
27 | 26 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β πΉ β π΄) |
28 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = πΉ β (πβπ‘) = (πΉβπ‘)) |
29 | 28 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π = πΉ β ((πβπ‘) Β· (πβπ‘)) = ((πβπ‘) Β· (πΉβπ‘))) |
30 | 29 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π = πΉ β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘)))) |
31 | 30 | eleq1d 2819 |
. . . . . . . 8
β’ (π = πΉ β ((π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄ β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄)) |
32 | 31 | imbi2d 341 |
. . . . . . 7
β’ (π = πΉ β (((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β ((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄))) |
33 | | stoweidlem2.2 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
34 | 33 | 3comr 1126 |
. . . . . . . 8
β’ ((π β π΄ β§ π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
35 | 34 | 3expib 1123 |
. . . . . . 7
β’ (π β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄)) |
36 | 32, 35 | vtoclga 3536 |
. . . . . 6
β’ (πΉ β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄)) |
37 | 27, 36 | mpcom 38 |
. . . . 5
β’ ((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄) |
38 | 37 | expcom 415 |
. . . 4
β’ (π β π΄ β (π β (π‘ β π β¦ ((πβπ‘) Β· (πΉβπ‘))) β π΄)) |
39 | 25, 38 | vtoclga 3536 |
. . 3
β’ ((π β π β¦ πΈ) β π΄ β (π β (π‘ β π β¦ (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘))) β π΄)) |
40 | 20, 39 | mpcom 38 |
. 2
β’ (π β (π‘ β π β¦ (((π β π β¦ πΈ)βπ‘) Β· (πΉβπ‘))) β π΄) |
41 | 11, 40 | eqeltrd 2834 |
1
β’ (π β (π‘ β π β¦ (πΈ Β· (πΉβπ‘))) β π΄) |