Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . . 5
β’ (β‘π· β β) = (β‘π· β β) |
2 | 1 | xmeter 24294 |
. . . 4
β’ (π· β (βMetβπ) β (β‘π· β β) Er π) |
3 | 2 | 3ad2ant1 1130 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β (β‘π· β β) Er π) |
4 | | simp3 1135 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β π΄ β (π(ballβπ·)+β)) |
5 | 1 | xmetec 24295 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π) β [π](β‘π· β β) = (π(ballβπ·)+β)) |
6 | 5 | 3adant3 1129 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β [π](β‘π· β β) = (π(ballβπ·)+β)) |
7 | 4, 6 | eleqtrrd 2830 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β π΄ β [π](β‘π· β β)) |
8 | | elecg 8748 |
. . . . . 6
β’ ((π΄ β (π(ballβπ·)+β) β§ π β π) β (π΄ β [π](β‘π· β β) β π(β‘π· β β)π΄)) |
9 | 8 | ancoms 458 |
. . . . 5
β’ ((π β π β§ π΄ β (π(ballβπ·)+β)) β (π΄ β [π](β‘π· β β) β π(β‘π· β β)π΄)) |
10 | 9 | 3adant1 1127 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β (π΄ β [π](β‘π· β β) β π(β‘π· β β)π΄)) |
11 | 7, 10 | mpbid 231 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β π(β‘π· β β)π΄) |
12 | 3, 11 | erthi 8756 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β [π](β‘π· β β) = [π΄](β‘π· β β)) |
13 | | pnfxr 11272 |
. . . . . 6
β’ +β
β β* |
14 | | blssm 24279 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ +β β β*)
β (π(ballβπ·)+β) β π) |
15 | 13, 14 | mp3an3 1446 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π) β (π(ballβπ·)+β) β π) |
16 | 15 | sselda 3977 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π΄ β (π(ballβπ·)+β)) β π΄ β π) |
17 | 1 | xmetec 24295 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΄ β π) β [π΄](β‘π· β β) = (π΄(ballβπ·)+β)) |
18 | 17 | adantlr 712 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π΄ β π) β [π΄](β‘π· β β) = (π΄(ballβπ·)+β)) |
19 | 16, 18 | syldan 590 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ π΄ β (π(ballβπ·)+β)) β [π΄](β‘π· β β) = (π΄(ballβπ·)+β)) |
20 | 19 | 3impa 1107 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β [π΄](β‘π· β β) = (π΄(ballβπ·)+β)) |
21 | 12, 6, 20 | 3eqtr3d 2774 |
1
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β (π(ballβπ·)+β) = (π΄(ballβπ·)+β)) |