Step | Hyp | Ref
| Expression |
1 | | ismidb.m |
. . 3
β’ (π β π β π) |
2 | | ismid.p |
. . . 4
β’ π = (BaseβπΊ) |
3 | | ismid.d |
. . . 4
β’ β =
(distβπΊ) |
4 | | ismid.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
5 | | eqid 2736 |
. . . 4
β’
(LineGβπΊ) =
(LineGβπΊ) |
6 | | ismid.g |
. . . 4
β’ (π β πΊ β TarskiG) |
7 | | ismidb.s |
. . . 4
β’ π = (pInvGβπΊ) |
8 | | midcl.1 |
. . . 4
β’ (π β π΄ β π) |
9 | | midcl.2 |
. . . 4
β’ (π β π΅ β π) |
10 | | ismid.1 |
. . . 4
β’ (π β πΊDimTarskiGβ₯2) |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | mideu 27566 |
. . 3
β’ (π β β!π β π π΅ = ((πβπ)βπ΄)) |
12 | | fveq2 6839 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
13 | 12 | fveq1d 6841 |
. . . . 5
β’ (π = π β ((πβπ)βπ΄) = ((πβπ)βπ΄)) |
14 | 13 | eqeq2d 2747 |
. . . 4
β’ (π = π β (π΅ = ((πβπ)βπ΄) β π΅ = ((πβπ)βπ΄))) |
15 | 14 | riota2 7335 |
. . 3
β’ ((π β π β§ β!π β π π΅ = ((πβπ)βπ΄)) β (π΅ = ((πβπ)βπ΄) β (β©π β π π΅ = ((πβπ)βπ΄)) = π)) |
16 | 1, 11, 15 | syl2anc 584 |
. 2
β’ (π β (π΅ = ((πβπ)βπ΄) β (β©π β π π΅ = ((πβπ)βπ΄)) = π)) |
17 | | df-mid 27602 |
. . . . 5
β’ midG =
(π β V β¦ (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)))) |
18 | | fveq2 6839 |
. . . . . . 7
β’ (π = πΊ β (Baseβπ) = (BaseβπΊ)) |
19 | 18, 2 | eqtr4di 2794 |
. . . . . 6
β’ (π = πΊ β (Baseβπ) = π) |
20 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (π = πΊ β (pInvGβπ) = (pInvGβπΊ)) |
21 | 20, 7 | eqtr4di 2794 |
. . . . . . . . . 10
β’ (π = πΊ β (pInvGβπ) = π) |
22 | 21 | fveq1d 6841 |
. . . . . . . . 9
β’ (π = πΊ β ((pInvGβπ)βπ) = (πβπ)) |
23 | 22 | fveq1d 6841 |
. . . . . . . 8
β’ (π = πΊ β (((pInvGβπ)βπ)βπ) = ((πβπ)βπ)) |
24 | 23 | eqeq2d 2747 |
. . . . . . 7
β’ (π = πΊ β (π = (((pInvGβπ)βπ)βπ) β π = ((πβπ)βπ))) |
25 | 19, 24 | riotaeqbidv 7312 |
. . . . . 6
β’ (π = πΊ β (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ)) = (β©π β π π = ((πβπ)βπ))) |
26 | 19, 19, 25 | mpoeq123dv 7428 |
. . . . 5
β’ (π = πΊ β (π β (Baseβπ), π β (Baseβπ) β¦ (β©π β (Baseβπ)π = (((pInvGβπ)βπ)βπ))) = (π β π, π β π β¦ (β©π β π π = ((πβπ)βπ)))) |
27 | 6 | elexd 3463 |
. . . . 5
β’ (π β πΊ β V) |
28 | 2 | fvexi 6853 |
. . . . . . 7
β’ π β V |
29 | 28, 28 | mpoex 8008 |
. . . . . 6
β’ (π β π, π β π β¦ (β©π β π π = ((πβπ)βπ))) β V |
30 | 29 | a1i 11 |
. . . . 5
β’ (π β (π β π, π β π β¦ (β©π β π π = ((πβπ)βπ))) β V) |
31 | 17, 26, 27, 30 | fvmptd3 6968 |
. . . 4
β’ (π β (midGβπΊ) = (π β π, π β π β¦ (β©π β π π = ((πβπ)βπ)))) |
32 | | simprr 771 |
. . . . . 6
β’ ((π β§ (π = π΄ β§ π = π΅)) β π = π΅) |
33 | | simprl 769 |
. . . . . . 7
β’ ((π β§ (π = π΄ β§ π = π΅)) β π = π΄) |
34 | 33 | fveq2d 6843 |
. . . . . 6
β’ ((π β§ (π = π΄ β§ π = π΅)) β ((πβπ)βπ) = ((πβπ)βπ΄)) |
35 | 32, 34 | eqeq12d 2752 |
. . . . 5
β’ ((π β§ (π = π΄ β§ π = π΅)) β (π = ((πβπ)βπ) β π΅ = ((πβπ)βπ΄))) |
36 | 35 | riotabidv 7311 |
. . . 4
β’ ((π β§ (π = π΄ β§ π = π΅)) β (β©π β π π = ((πβπ)βπ)) = (β©π β π π΅ = ((πβπ)βπ΄))) |
37 | | riotacl 7327 |
. . . . 5
β’
(β!π β
π π΅ = ((πβπ)βπ΄) β (β©π β π π΅ = ((πβπ)βπ΄)) β π) |
38 | 11, 37 | syl 17 |
. . . 4
β’ (π β (β©π β π π΅ = ((πβπ)βπ΄)) β π) |
39 | 31, 36, 8, 9, 38 | ovmpod 7503 |
. . 3
β’ (π β (π΄(midGβπΊ)π΅) = (β©π β π π΅ = ((πβπ)βπ΄))) |
40 | 39 | eqeq1d 2738 |
. 2
β’ (π β ((π΄(midGβπΊ)π΅) = π β (β©π β π π΅ = ((πβπ)βπ΄)) = π)) |
41 | 16, 40 | bitr4d 281 |
1
β’ (π β (π΅ = ((πβπ)βπ΄) β (π΄(midGβπΊ)π΅) = π)) |