Step | Hyp | Ref
| Expression |
1 | | df-br 5110 |
. . 3
β’ (π΄(βGβπΊ)π΅ β β¨π΄, π΅β© β (βGβπΊ)) |
2 | | df-perpg 27687 |
. . . . 5
β’ βG
= (π β V β¦
{β¨π, πβ© β£ ((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ))}) |
3 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π = πΊ) β π = πΊ) |
4 | 3 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π β§ π = πΊ) β (LineGβπ) = (LineGβπΊ)) |
5 | | isperp.l |
. . . . . . . . . . 11
β’ πΏ = (LineGβπΊ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . . . . 10
β’ ((π β§ π = πΊ) β (LineGβπ) = πΏ) |
7 | 6 | rneqd 5897 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β ran (LineGβπ) = ran πΏ) |
8 | 7 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (π β ran (LineGβπ) β π β ran πΏ)) |
9 | 7 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (π β ran (LineGβπ) β π β ran πΏ)) |
10 | 8, 9 | anbi12d 632 |
. . . . . . 7
β’ ((π β§ π = πΊ) β ((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β (π β ran πΏ β§ π β ran πΏ))) |
11 | 3 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π = πΊ) β (βGβπ) = (βGβπΊ)) |
12 | 11 | eleq2d 2820 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β (β¨βπ’π₯π£ββ© β (βGβπ) β β¨βπ’π₯π£ββ© β (βGβπΊ))) |
13 | 12 | ralbidv 3171 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ) β βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))) |
14 | 13 | rexralbidv 3211 |
. . . . . . 7
β’ ((π β§ π = πΊ) β (βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ) β βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))) |
15 | 10, 14 | anbi12d 632 |
. . . . . 6
β’ ((π β§ π = πΊ) β (((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ)) β ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ)))) |
16 | 15 | opabbidv 5175 |
. . . . 5
β’ ((π β§ π = πΊ) β {β¨π, πβ© β£ ((π β ran (LineGβπ) β§ π β ran (LineGβπ)) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπ))} = {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))}) |
17 | | isperp.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
18 | 17 | elexd 3467 |
. . . . 5
β’ (π β πΊ β V) |
19 | 5 | fvexi 6860 |
. . . . . . . 8
β’ πΏ β V |
20 | | rnexg 7845 |
. . . . . . . 8
β’ (πΏ β V β ran πΏ β V) |
21 | 19, 20 | mp1i 13 |
. . . . . . 7
β’ (π β ran πΏ β V) |
22 | 21, 21 | xpexd 7689 |
. . . . . 6
β’ (π β (ran πΏ Γ ran πΏ) β V) |
23 | | opabssxp 5728 |
. . . . . . 7
β’
{β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β (ran πΏ Γ ran πΏ) |
24 | 23 | a1i 11 |
. . . . . 6
β’ (π β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β (ran πΏ Γ ran πΏ)) |
25 | 22, 24 | ssexd 5285 |
. . . . 5
β’ (π β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β V) |
26 | 2, 16, 18, 25 | fvmptd2 6960 |
. . . 4
β’ (π β (βGβπΊ) = {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))}) |
27 | 26 | eleq2d 2820 |
. . 3
β’ (π β (β¨π΄, π΅β© β (βGβπΊ) β β¨π΄, π΅β© β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))})) |
28 | 1, 27 | bitrid 283 |
. 2
β’ (π β (π΄(βGβπΊ)π΅ β β¨π΄, π΅β© β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))})) |
29 | | isperp.a |
. . 3
β’ (π β π΄ β ran πΏ) |
30 | | isperp.b |
. . 3
β’ (π β π΅ β ran πΏ) |
31 | | ineq12 4171 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β (π β© π) = (π΄ β© π΅)) |
32 | | simpll 766 |
. . . . . 6
β’ (((π = π΄ β§ π = π΅) β§ π₯ β (π β© π)) β π = π΄) |
33 | | simpllr 775 |
. . . . . . 7
β’ ((((π = π΄ β§ π = π΅) β§ π₯ β (π β© π)) β§ π’ β π) β π = π΅) |
34 | 33 | raleqdv 3312 |
. . . . . 6
β’ ((((π = π΄ β§ π = π΅) β§ π₯ β (π β© π)) β§ π’ β π) β (βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ) β βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) |
35 | 32, 34 | raleqbidva 3320 |
. . . . 5
β’ (((π = π΄ β§ π = π΅) β§ π₯ β (π β© π)) β (βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ) β βπ’ β π΄ βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) |
36 | 31, 35 | rexeqbidva 3321 |
. . . 4
β’ ((π = π΄ β§ π = π΅) β (βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ) β βπ₯ β (π΄ β© π΅)βπ’ β π΄ βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) |
37 | 36 | opelopab2a 5496 |
. . 3
β’ ((π΄ β ran πΏ β§ π΅ β ran πΏ) β (β¨π΄, π΅β© β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β βπ₯ β (π΄ β© π΅)βπ’ β π΄ βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) |
38 | 29, 30, 37 | syl2anc 585 |
. 2
β’ (π β (β¨π΄, π΅β© β {β¨π, πβ© β£ ((π β ran πΏ β§ π β ran πΏ) β§ βπ₯ β (π β© π)βπ’ β π βπ£ β π β¨βπ’π₯π£ββ© β (βGβπΊ))} β βπ₯ β (π΄ β© π΅)βπ’ β π΄ βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) |
39 | 28, 38 | bitrd 279 |
1
β’ (π β (π΄(βGβπΊ)π΅ β βπ₯ β (π΄ β© π΅)βπ’ β π΄ βπ£ β π΅ β¨βπ’π₯π£ββ© β (βGβπΊ))) |