Step | Hyp | Ref
| Expression |
1 | | hypcgr.p |
. . . 4
β’ π = (BaseβπΊ) |
2 | | hypcgr.m |
. . . 4
β’ β =
(distβπΊ) |
3 | | hypcgr.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
4 | | hypcgr.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
5 | 4 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΊ β TarskiG) |
6 | | hypcgr.h |
. . . . 5
β’ (π β πΊDimTarskiGβ₯2) |
7 | 6 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΊDimTarskiGβ₯2) |
8 | | hypcgr.a |
. . . . 5
β’ (π β π΄ β π) |
9 | 8 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β π΄ β π) |
10 | | hypcgr.b |
. . . . 5
β’ (π β π΅ β π) |
11 | 10 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β π΅ β π) |
12 | | hypcgr.c |
. . . . 5
β’ (π β πΆ β π) |
13 | 12 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΆ β π) |
14 | | eqid 2732 |
. . . . 5
β’
(LineGβπΊ) =
(LineGβπΊ) |
15 | | eqid 2732 |
. . . . 5
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
16 | | eqid 2732 |
. . . . 5
β’
((pInvGβπΊ)βπ΅) = ((pInvGβπΊ)βπ΅) |
17 | | hypcgr.d |
. . . . . 6
β’ (π β π· β π) |
18 | 17 | adantr 481 |
. . . . 5
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β π· β π) |
19 | 1, 2, 3, 14, 15, 5, 11, 16, 18 | mircl 27901 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (((pInvGβπΊ)βπ΅)βπ·) β π) |
20 | | hypcgr.e |
. . . . 5
β’ (π β πΈ β π) |
21 | 20 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΈ β π) |
22 | | hypcgr.1 |
. . . . 5
β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
23 | 22 | adantr 481 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
24 | | eqidd 2733 |
. . . . . 6
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (((pInvGβπΊ)βπ΅)βπ·) = (((pInvGβπΊ)βπ΅)βπ·)) |
25 | | hypcgrlem2.b |
. . . . . . . . 9
β’ (π β π΅ = πΈ) |
26 | 25 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β π΅ = πΈ) |
27 | 1, 2, 3, 14, 15, 5, 11, 16, 21 | mirinv 27906 |
. . . . . . . 8
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β ((((pInvGβπΊ)βπ΅)βπΈ) = πΈ β π΅ = πΈ)) |
28 | 26, 27 | mpbird 256 |
. . . . . . 7
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (((pInvGβπΊ)βπ΅)βπΈ) = πΈ) |
29 | 28 | eqcomd 2738 |
. . . . . 6
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΈ = (((pInvGβπΊ)βπ΅)βπΈ)) |
30 | | hypcgr.f |
. . . . . . . . . 10
β’ (π β πΉ β π) |
31 | 30 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΉ β π) |
32 | 1, 2, 3, 5, 7, 13,
31 | midcom 28022 |
. . . . . . . 8
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (πΆ(midGβπΊ)πΉ) = (πΉ(midGβπΊ)πΆ)) |
33 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (πΆ(midGβπΊ)πΉ) = π΅) |
34 | 32, 33 | eqtr3d 2774 |
. . . . . . 7
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (πΉ(midGβπΊ)πΆ) = π΅) |
35 | 1, 2, 3, 5, 7, 31,
13, 15, 11 | ismidb 28018 |
. . . . . . 7
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (πΆ = (((pInvGβπΊ)βπ΅)βπΉ) β (πΉ(midGβπΊ)πΆ) = π΅)) |
36 | 34, 35 | mpbird 256 |
. . . . . 6
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΆ = (((pInvGβπΊ)βπ΅)βπΉ)) |
37 | 24, 29, 36 | s3eqd 14811 |
. . . . 5
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β β¨β(((pInvGβπΊ)βπ΅)βπ·)πΈπΆββ© =
β¨β(((pInvGβπΊ)βπ΅)βπ·)(((pInvGβπΊ)βπ΅)βπΈ)(((pInvGβπΊ)βπ΅)βπΉ)ββ©) |
38 | | hypcgr.2 |
. . . . . . 7
β’ (π β β¨βπ·πΈπΉββ© β (βGβπΊ)) |
39 | 38 | adantr 481 |
. . . . . 6
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β β¨βπ·πΈπΉββ© β (βGβπΊ)) |
40 | 1, 2, 3, 14, 15, 5, 18, 21, 31, 39, 16, 11 | mirrag 27941 |
. . . . 5
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β β¨β(((pInvGβπΊ)βπ΅)βπ·)(((pInvGβπΊ)βπ΅)βπΈ)(((pInvGβπΊ)βπ΅)βπΉ)ββ© β (βGβπΊ)) |
41 | 37, 40 | eqeltrd 2833 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β β¨β(((pInvGβπΊ)βπ΅)βπ·)πΈπΆββ© β (βGβπΊ)) |
42 | | hypcgr.3 |
. . . . . 6
β’ (π β (π΄ β π΅) = (π· β πΈ)) |
43 | 42 | adantr 481 |
. . . . 5
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (π΄ β π΅) = (π· β πΈ)) |
44 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 21 | miriso 27910 |
. . . . 5
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β ((((pInvGβπΊ)βπ΅)βπ·) β (((pInvGβπΊ)βπ΅)βπΈ)) = (π· β πΈ)) |
45 | 28 | oveq2d 7421 |
. . . . 5
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β ((((pInvGβπΊ)βπ΅)βπ·) β (((pInvGβπΊ)βπ΅)βπΈ)) = ((((pInvGβπΊ)βπ΅)βπ·) β πΈ)) |
46 | 43, 44, 45 | 3eqtr2d 2778 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (π΄ β π΅) = ((((pInvGβπΊ)βπ΅)βπ·) β πΈ)) |
47 | 26 | oveq1d 7420 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (π΅ β πΆ) = (πΈ β πΆ)) |
48 | | eqid 2732 |
. . . 4
β’
((lInvGβπΊ)β((π΄(midGβπΊ)(((pInvGβπΊ)βπ΅)βπ·))(LineGβπΊ)π΅)) = ((lInvGβπΊ)β((π΄(midGβπΊ)(((pInvGβπΊ)βπ΅)βπ·))(LineGβπΊ)π΅)) |
49 | | eqidd 2733 |
. . . 4
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β πΆ = πΆ) |
50 | 1, 2, 3, 5, 7, 9, 11, 13, 19, 21, 13, 23, 41, 46, 47, 26, 48, 49 | hypcgrlem1 28039 |
. . 3
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (π΄ β πΆ) = ((((pInvGβπΊ)βπ΅)βπ·) β πΆ)) |
51 | 36 | oveq2d 7421 |
. . 3
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β ((((pInvGβπΊ)βπ΅)βπ·) β πΆ) = ((((pInvGβπΊ)βπ΅)βπ·) β (((pInvGβπΊ)βπ΅)βπΉ))) |
52 | 1, 2, 3, 14, 15, 5, 11, 16, 18, 31 | miriso 27910 |
. . 3
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β ((((pInvGβπΊ)βπ΅)βπ·) β (((pInvGβπΊ)βπ΅)βπΉ)) = (π· β πΉ)) |
53 | 50, 51, 52 | 3eqtrd 2776 |
. 2
β’ ((π β§ (πΆ(midGβπΊ)πΉ) = π΅) β (π΄ β πΆ) = (π· β πΉ)) |
54 | 4 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β πΊ β TarskiG) |
55 | 6 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β πΊDimTarskiGβ₯2) |
56 | 8 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β π΄ β π) |
57 | 10 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β π΅ β π) |
58 | 12 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β πΆ β π) |
59 | 17 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β π· β π) |
60 | 20 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β πΈ β π) |
61 | 30 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β πΉ β π) |
62 | 22 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
63 | 38 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β β¨βπ·πΈπΉββ© β (βGβπΊ)) |
64 | 42 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β (π΄ β π΅) = (π· β πΈ)) |
65 | | hypcgr.4 |
. . . . 5
β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) |
66 | 65 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β (π΅ β πΆ) = (πΈ β πΉ)) |
67 | 25 | ad2antrr 724 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β π΅ = πΈ) |
68 | | eqid 2732 |
. . . 4
β’
((lInvGβπΊ)β((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) = ((lInvGβπΊ)β((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) |
69 | | simpr 485 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β πΆ = πΉ) |
70 | 1, 2, 3, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 66, 67, 68, 69 | hypcgrlem1 28039 |
. . 3
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = πΉ) β (π΄ β πΆ) = (π· β πΉ)) |
71 | 4 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΊ β TarskiG) |
72 | 6 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΊDimTarskiGβ₯2) |
73 | 8 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π΄ β π) |
74 | 10 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π΅ β π) |
75 | 12 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΆ β π) |
76 | | hypcgrlem2.s |
. . . . . 6
β’ π = ((lInvGβπΊ)β((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)) |
77 | 30 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΉ β π) |
78 | 1, 2, 3, 71, 72, 75, 77 | midcl 28017 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β π) |
79 | | simplr 767 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β π΅) |
80 | 1, 3, 14, 71, 78, 74, 79 | tgelrnln 27870 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β ((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅) β ran (LineGβπΊ)) |
81 | 17 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π· β π) |
82 | 1, 2, 3, 71, 72, 76, 14, 80, 81 | lmicl 28026 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πβπ·) β π) |
83 | 20 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΈ β π) |
84 | 1, 2, 3, 71, 72, 76, 14, 80, 83 | lmicl 28026 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πβπΈ) β π) |
85 | 1, 2, 3, 71, 72, 76, 14, 80, 77 | lmicl 28026 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πβπΉ) β π) |
86 | 22 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
87 | 1, 2, 3, 71, 72, 76, 14, 80 | lmimot 28038 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π β (πΊIsmtπΊ)) |
88 | 38 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β β¨βπ·πΈπΉββ© β (βGβπΊ)) |
89 | 1, 2, 3, 14, 15, 71, 81, 83, 77, 87, 88 | motrag 27948 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β β¨β(πβπ·)(πβπΈ)(πβπΉ)ββ© β (βGβπΊ)) |
90 | 42 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΄ β π΅) = (π· β πΈ)) |
91 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 83 | lmiiso 28037 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β ((πβπ·) β (πβπΈ)) = (π· β πΈ)) |
92 | 90, 91 | eqtr4d 2775 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΄ β π΅) = ((πβπ·) β (πβπΈ))) |
93 | 65 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΅ β πΆ) = (πΈ β πΉ)) |
94 | 1, 2, 3, 71, 72, 76, 14, 80, 83, 77 | lmiiso 28037 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β ((πβπΈ) β (πβπΉ)) = (πΈ β πΉ)) |
95 | 93, 94 | eqtr4d 2775 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΅ β πΆ) = ((πβπΈ) β (πβπΉ))) |
96 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx2 27874 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π΅ β ((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)) |
97 | 1, 2, 3, 71, 72, 76, 14, 80, 74, 96 | lmicinv 28033 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πβπ΅) = π΅) |
98 | 25 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π΅ = πΈ) |
99 | 98 | fveq2d 6892 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πβπ΅) = (πβπΈ)) |
100 | 97, 99 | eqtr3d 2774 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π΅ = (πβπΈ)) |
101 | | eqid 2732 |
. . . . 5
β’
((lInvGβπΊ)β((π΄(midGβπΊ)(πβπ·))(LineGβπΊ)π΅)) = ((lInvGβπΊ)β((π΄(midGβπΊ)(πβπ·))(LineGβπΊ)π΅)) |
102 | 1, 2, 3, 71, 72, 75, 77 | midcom 28022 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) = (πΉ(midGβπΊ)πΆ)) |
103 | 1, 3, 14, 71, 78, 74, 79 | tglinerflx1 27873 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β ((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)) |
104 | 102, 103 | eqeltrrd 2834 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΉ(midGβπΊ)πΆ) β ((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)) |
105 | | simpr 485 |
. . . . . . . . . 10
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΆ β πΉ) |
106 | 105 | necomd 2996 |
. . . . . . . . 9
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΉ β πΆ) |
107 | 1, 3, 14, 71, 77, 75, 106 | tgelrnln 27870 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΉ(LineGβπΊ)πΆ) β ran (LineGβπΊ)) |
108 | 1, 2, 3, 71, 72, 75, 77 | midbtwn 28019 |
. . . . . . . . . . 11
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β (πΆπΌπΉ)) |
109 | 1, 2, 3, 71, 75, 78, 77, 108 | tgbtwncom 27728 |
. . . . . . . . . 10
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β (πΉπΌπΆ)) |
110 | 1, 3, 14, 71, 77, 75, 78, 106, 109 | btwnlng1 27859 |
. . . . . . . . 9
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β (πΉ(LineGβπΊ)πΆ)) |
111 | 103, 110 | elind 4193 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) β (((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅) β© (πΉ(LineGβπΊ)πΆ))) |
112 | 1, 3, 14, 71, 77, 75, 106 | tglinerflx2 27874 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΆ β (πΉ(LineGβπΊ)πΆ)) |
113 | 79 | necomd 2996 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β π΅ β (πΆ(midGβπΊ)πΉ)) |
114 | 4 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β πΊ β TarskiG) |
115 | 12 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β πΆ β π) |
116 | 30 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β πΉ β π) |
117 | 6 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β πΊDimTarskiGβ₯2) |
118 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β πΆ = (πΆ(midGβπΊ)πΉ)) |
119 | 118 | eqcomd 2738 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β (πΆ(midGβπΊ)πΉ) = πΆ) |
120 | 1, 2, 3, 114, 117, 115, 116, 119 | midcgr 28020 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β (πΆ β πΆ) = (πΆ β πΉ)) |
121 | 120 | eqcomd 2738 |
. . . . . . . . . . . 12
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β (πΆ β πΉ) = (πΆ β πΆ)) |
122 | 1, 2, 3, 114, 115, 116, 115, 121 | axtgcgrid 27703 |
. . . . . . . . . . 11
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ = (πΆ(midGβπΊ)πΉ)) β πΆ = πΉ) |
123 | 122 | ex 413 |
. . . . . . . . . 10
β’ ((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β (πΆ = (πΆ(midGβπΊ)πΉ) β πΆ = πΉ)) |
124 | 123 | necon3d 2961 |
. . . . . . . . 9
β’ ((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β (πΆ β πΉ β πΆ β (πΆ(midGβπΊ)πΉ))) |
125 | 124 | imp 407 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΆ β (πΆ(midGβπΊ)πΉ)) |
126 | 98 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΈ = π΅) |
127 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ(midGβπΊ)πΉ) = (πΆ(midGβπΊ)πΉ)) |
128 | 1, 2, 3, 71, 72, 75, 77, 15, 78 | ismidb 28018 |
. . . . . . . . . . . 12
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΉ = (((pInvGβπΊ)β(πΆ(midGβπΊ)πΉ))βπΆ) β (πΆ(midGβπΊ)πΉ) = (πΆ(midGβπΊ)πΉ))) |
129 | 127, 128 | mpbird 256 |
. . . . . . . . . . 11
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΉ = (((pInvGβπΊ)β(πΆ(midGβπΊ)πΉ))βπΆ)) |
130 | 126, 129 | oveq12d 7423 |
. . . . . . . . . 10
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΈ β πΉ) = (π΅ β (((pInvGβπΊ)β(πΆ(midGβπΊ)πΉ))βπΆ))) |
131 | 93, 130 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΅ β πΆ) = (π΅ β (((pInvGβπΊ)β(πΆ(midGβπΊ)πΉ))βπΆ))) |
132 | 1, 2, 3, 14, 15, 71, 74, 78, 75 | israg 27937 |
. . . . . . . . 9
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (β¨βπ΅(πΆ(midGβπΊ)πΉ)πΆββ© β (βGβπΊ) β (π΅ β πΆ) = (π΅ β (((pInvGβπΊ)β(πΆ(midGβπΊ)πΉ))βπΆ)))) |
133 | 131, 132 | mpbird 256 |
. . . . . . . 8
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β β¨βπ΅(πΆ(midGβπΊ)πΉ)πΆββ© β (βGβπΊ)) |
134 | 1, 2, 3, 14, 71, 80, 107, 111, 96, 112, 113, 125, 133 | ragperp 27957 |
. . . . . . 7
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β ((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)(βGβπΊ)(πΉ(LineGβπΊ)πΆ)) |
135 | 134 | orcd 871 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)(βGβπΊ)(πΉ(LineGβπΊ)πΆ) β¨ πΉ = πΆ)) |
136 | 1, 2, 3, 71, 72, 76, 14, 80, 77, 75 | islmib 28027 |
. . . . . 6
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (πΆ = (πβπΉ) β ((πΉ(midGβπΊ)πΆ) β ((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅) β§ (((πΆ(midGβπΊ)πΉ)(LineGβπΊ)π΅)(βGβπΊ)(πΉ(LineGβπΊ)πΆ) β¨ πΉ = πΆ)))) |
137 | 104, 135,
136 | mpbir2and 711 |
. . . . 5
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β πΆ = (πβπΉ)) |
138 | 1, 2, 3, 71, 72, 73, 74, 75, 82, 84, 85, 86, 89, 92, 95, 100, 101, 137 | hypcgrlem1 28039 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΄ β πΆ) = ((πβπ·) β (πβπΉ))) |
139 | 1, 2, 3, 71, 72, 76, 14, 80, 81, 77 | lmiiso 28037 |
. . . 4
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β ((πβπ·) β (πβπΉ)) = (π· β πΉ)) |
140 | 138, 139 | eqtrd 2772 |
. . 3
β’ (((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β§ πΆ β πΉ) β (π΄ β πΆ) = (π· β πΉ)) |
141 | 70, 140 | pm2.61dane 3029 |
. 2
β’ ((π β§ (πΆ(midGβπΊ)πΉ) β π΅) β (π΄ β πΆ) = (π· β πΉ)) |
142 | 53, 141 | pm2.61dane 3029 |
1
β’ (π β (π΄ β πΆ) = (π· β πΉ)) |