Step | Hyp | Ref
| Expression |
1 | | df-ov 7409 |
. 2
β’
(β¨π΄, π΅β©TransportToβ¨πΆ, π·β©) =
(TransportToββ¨β¨π΄, π΅β©, β¨πΆ, π·β©β©) |
2 | | opelxpi 5713 |
. . . . . . 7
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ))) |
3 | 2 | 3ad2ant1 1134 |
. . . . . 6
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ))) |
4 | | opelxpi 5713 |
. . . . . . 7
β’ ((πΆ β (πΌβπ) β§ π· β (πΌβπ)) β β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ))) |
5 | 4 | 3ad2ant2 1135 |
. . . . . 6
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ))) |
6 | | simp3 1139 |
. . . . . . 7
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β πΆ β π·) |
7 | | op1stg 7984 |
. . . . . . . 8
β’ ((πΆ β (πΌβπ) β§ π· β (πΌβπ)) β (1st ββ¨πΆ, π·β©) = πΆ) |
8 | 7 | 3ad2ant2 1135 |
. . . . . . 7
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (1st ββ¨πΆ, π·β©) = πΆ) |
9 | | op2ndg 7985 |
. . . . . . . 8
β’ ((πΆ β (πΌβπ) β§ π· β (πΌβπ)) β (2nd ββ¨πΆ, π·β©) = π·) |
10 | 9 | 3ad2ant2 1135 |
. . . . . . 7
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (2nd ββ¨πΆ, π·β©) = π·) |
11 | 6, 8, 10 | 3netr4d 3019 |
. . . . . 6
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (1st ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) |
12 | 3, 5, 11 | 3jca 1129 |
. . . . 5
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©))) |
13 | 8 | opeq1d 4879 |
. . . . . . . . 9
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β β¨(1st
ββ¨πΆ, π·β©), πβ© = β¨πΆ, πβ©) |
14 | 10, 13 | breq12d 5161 |
. . . . . . . 8
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β ((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β π· Btwn β¨πΆ, πβ©)) |
15 | 10 | opeq1d 4879 |
. . . . . . . . 9
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β β¨(2nd
ββ¨πΆ, π·β©), πβ© = β¨π·, πβ©) |
16 | 15 | breq1d 5158 |
. . . . . . . 8
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β© β β¨π·, πβ©Cgrβ¨π΄, π΅β©)) |
17 | 14, 16 | anbi12d 632 |
. . . . . . 7
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (((2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©) β (π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) |
18 | 17 | riotabidv 7364 |
. . . . . 6
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) |
19 | 18 | eqcomd 2739 |
. . . . 5
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) |
20 | 12, 19 | jca 513 |
. . . 4
β’ (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·) β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
21 | | fveq2 6889 |
. . . . . . . . 9
β’ (π = π β (πΌβπ) = (πΌβπ)) |
22 | 21 | sqxpeqd 5708 |
. . . . . . . 8
β’ (π = π β ((πΌβπ) Γ (πΌβπ)) = ((πΌβπ) Γ (πΌβπ))) |
23 | 22 | eleq2d 2820 |
. . . . . . 7
β’ (π = π β (β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)))) |
24 | 22 | eleq2d 2820 |
. . . . . . 7
β’ (π = π β (β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)))) |
25 | 23, 24 | 3anbi12d 1438 |
. . . . . 6
β’ (π = π β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β (β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)))) |
26 | 21 | riotaeqdv 7363 |
. . . . . . 7
β’ (π = π β (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) |
27 | 26 | eqeq2d 2744 |
. . . . . 6
β’ (π = π β ((β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)) β (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
28 | 25, 27 | anbi12d 632 |
. . . . 5
β’ (π = π β (((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))))) |
29 | 28 | rspcev 3613 |
. . . 4
β’ ((π β β β§
((β¨π΄, π΅β© β
((πΌβπ) Γ
(πΌβπ)) β§
β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
30 | 20, 29 | sylan2 594 |
. . 3
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
31 | | df-br 5149 |
. . . . 5
β’
(β¨β¨π΄,
π΅β©, β¨πΆ, π·β©β©TransportTo(β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β β¨β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©, (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))β© β
TransportTo) |
32 | | df-transport 34991 |
. . . . . 6
β’
TransportTo = {β¨β¨π, πβ©, π₯β© β£ βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ)))} |
33 | 32 | eleq2i 2826 |
. . . . 5
β’
(β¨β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©, (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))β© β TransportTo β
β¨β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©, (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))β© β {β¨β¨π, πβ©, π₯β© β£ βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ)))}) |
34 | | opex 5464 |
. . . . . 6
β’
β¨π΄, π΅β© β V |
35 | | opex 5464 |
. . . . . 6
β’
β¨πΆ, π·β© β V |
36 | | riotaex 7366 |
. . . . . 6
β’
(β©π
β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β V |
37 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = β¨π΄, π΅β© β (π β ((πΌβπ) Γ (πΌβπ)) β β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)))) |
38 | 37 | 3anbi1d 1441 |
. . . . . . . . 9
β’ (π = β¨π΄, π΅β© β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β
(β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)))) |
39 | | breq2 5152 |
. . . . . . . . . . . 12
β’ (π = β¨π΄, π΅β© β (β¨(2nd
βπ), πβ©Cgrπ β β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©)) |
40 | 39 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = β¨π΄, π΅β© β (((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ) β ((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©))) |
41 | 40 | riotabidv 7364 |
. . . . . . . . . 10
β’ (π = β¨π΄, π΅β© β (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ)) = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st βπ), πβ© β§ β¨(2nd
βπ), πβ©Cgrβ¨π΄, π΅β©))) |
42 | 41 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = β¨π΄, π΅β© β (π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st βπ), πβ© β§ β¨(2nd
βπ), πβ©Cgrπ)) β π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st βπ), πβ© β§ β¨(2nd
βπ), πβ©Cgrβ¨π΄, π΅β©)))) |
43 | 38, 42 | anbi12d 632 |
. . . . . . . 8
β’ (π = β¨π΄, π΅β© β (((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ))) β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©))))) |
44 | 43 | rexbidv 3179 |
. . . . . . 7
β’ (π = β¨π΄, π΅β© β (βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ))) β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©))))) |
45 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = β¨πΆ, π·β© β (π β ((πΌβπ) Γ (πΌβπ)) β β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)))) |
46 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (π = β¨πΆ, π·β© β (1st βπ) = (1st
ββ¨πΆ, π·β©)) |
47 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (π = β¨πΆ, π·β© β (2nd βπ) = (2nd
ββ¨πΆ, π·β©)) |
48 | 46, 47 | neeq12d 3003 |
. . . . . . . . . 10
β’ (π = β¨πΆ, π·β© β ((1st βπ) β (2nd
βπ) β
(1st ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©))) |
49 | 45, 48 | 3anbi23d 1440 |
. . . . . . . . 9
β’ (π = β¨πΆ, π·β© β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β
(β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)))) |
50 | 46 | opeq1d 4879 |
. . . . . . . . . . . . 13
β’ (π = β¨πΆ, π·β© β β¨(1st
βπ), πβ© = β¨(1st
ββ¨πΆ, π·β©), πβ©) |
51 | 47, 50 | breq12d 5161 |
. . . . . . . . . . . 12
β’ (π = β¨πΆ, π·β© β ((2nd βπ) Btwn β¨(1st
βπ), πβ© β (2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ©)) |
52 | 47 | opeq1d 4879 |
. . . . . . . . . . . . 13
β’ (π = β¨πΆ, π·β© β β¨(2nd
βπ), πβ© = β¨(2nd
ββ¨πΆ, π·β©), πβ©) |
53 | 52 | breq1d 5158 |
. . . . . . . . . . . 12
β’ (π = β¨πΆ, π·β© β (β¨(2nd
βπ), πβ©Cgrβ¨π΄, π΅β© β β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)) |
54 | 51, 53 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = β¨πΆ, π·β© β (((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©) β ((2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) |
55 | 54 | riotabidv 7364 |
. . . . . . . . . 10
β’ (π = β¨πΆ, π·β© β (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) |
56 | 55 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = β¨πΆ, π·β© β (π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st βπ), πβ© β§ β¨(2nd
βπ), πβ©Cgrβ¨π΄, π΅β©)) β π₯ = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
57 | 49, 56 | anbi12d 632 |
. . . . . . . 8
β’ (π = β¨πΆ, π·β© β (((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©))) β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§ π₯ = (β©π β (πΌβπ)((2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))))) |
58 | 57 | rexbidv 3179 |
. . . . . . 7
β’ (π = β¨πΆ, π·β© β (βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrβ¨π΄, π΅β©))) β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§ π₯ = (β©π β (πΌβπ)((2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))))) |
59 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π₯ = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β (π₯ = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)) β (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
60 | 59 | anbi2d 630 |
. . . . . . . 8
β’ (π₯ = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β (((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§ π₯ = (β©π β (πΌβπ)((2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))))) |
61 | 60 | rexbidv 3179 |
. . . . . . 7
β’ (π₯ = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β (βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§ π₯ = (β©π β (πΌβπ)((2nd
ββ¨πΆ, π·β©) Btwn
β¨(1st ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))))) |
62 | 44, 58, 61 | eloprabg 7515 |
. . . . . 6
β’
((β¨π΄, π΅β© β V β§
β¨πΆ, π·β© β V β§ (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β V) β
(β¨β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©, (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))β© β {β¨β¨π, πβ©, π₯β© β£ βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ)))} β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))))) |
63 | 34, 35, 36, 62 | mp3an 1462 |
. . . . 5
β’
(β¨β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©, (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))β© β {β¨β¨π, πβ©, π₯β© β£ βπ β β ((π β ((πΌβπ) Γ (πΌβπ)) β§ π β ((πΌβπ) Γ (πΌβπ)) β§ (1st βπ) β (2nd
βπ)) β§ π₯ = (β©π β (πΌβπ)((2nd βπ) Btwn β¨(1st
βπ), πβ© β§
β¨(2nd βπ), πβ©Cgrπ)))} β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
64 | 31, 33, 63 | 3bitri 297 |
. . . 4
β’
(β¨β¨π΄,
π΅β©, β¨πΆ, π·β©β©TransportTo(β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β βπ β β ((β¨π΄, π΅β© β ((πΌβπ) Γ (πΌβπ)) β§ β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©)))) |
65 | | funtransport 34992 |
. . . . 5
β’ Fun
TransportTo |
66 | | funbrfv 6940 |
. . . . 5
β’ (Fun
TransportTo β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©TransportTo(β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β
(TransportToββ¨β¨π΄, π΅β©, β¨πΆ, π·β©β©) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)))) |
67 | 65, 66 | ax-mp 5 |
. . . 4
β’
(β¨β¨π΄,
π΅β©, β¨πΆ, π·β©β©TransportTo(β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) β
(TransportToββ¨β¨π΄, π΅β©, β¨πΆ, π·β©β©) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) |
68 | 64, 67 | sylbir 234 |
. . 3
β’
(βπ β
β ((β¨π΄, π΅β© β
((πΌβπ) Γ
(πΌβπ)) β§
β¨πΆ, π·β© β ((πΌβπ) Γ (πΌβπ)) β§ (1st
ββ¨πΆ, π·β©) β (2nd
ββ¨πΆ, π·β©)) β§
(β©π β
(πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) = (β©π β (πΌβπ)((2nd ββ¨πΆ, π·β©) Btwn β¨(1st
ββ¨πΆ, π·β©), πβ© β§ β¨(2nd
ββ¨πΆ, π·β©), πβ©Cgrβ¨π΄, π΅β©))) β
(TransportToββ¨β¨π΄, π΅β©, β¨πΆ, π·β©β©) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) |
69 | 30, 68 | syl 17 |
. 2
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β
(TransportToββ¨β¨π΄, π΅β©, β¨πΆ, π·β©β©) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) |
70 | 1, 69 | eqtrid 2785 |
1
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β (β¨π΄, π΅β©TransportToβ¨πΆ, π·β©) = (β©π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©))) |