Step | Hyp | Ref
| Expression |
1 | | krippen.1 |
. . . 4
β’ (π β πΆ β (π΄πΌπΈ)) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ πΈ = πΆ) β πΆ β (π΄πΌπΈ)) |
3 | | mirval.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
4 | | mirval.d |
. . . . . . 7
β’ β =
(distβπΊ) |
5 | | mirval.i |
. . . . . . 7
β’ πΌ = (ItvβπΊ) |
6 | | mirval.g |
. . . . . . . 8
β’ (π β πΊ β TarskiG) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β πΊ β TarskiG) |
8 | | krippen.c |
. . . . . . . 8
β’ (π β πΆ β π) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β πΆ β π) |
10 | | krippen.a |
. . . . . . . 8
β’ (π β π΄ β π) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β π΄ β π) |
12 | | krippen.b |
. . . . . . . 8
β’ (π β π΅ β π) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β π΅ β π) |
14 | | krippen.3 |
. . . . . . . 8
β’ (π β (πΆ β π΄) = (πΆ β π΅)) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β (πΆ β π΄) = (πΆ β π΅)) |
16 | | krippen.l |
. . . . . . . 8
β’ β€ =
(β€GβπΊ) |
17 | | krippen.7 |
. . . . . . . . . 10
β’ (π β (πΆ β π΄) β€ (πΆ β πΈ)) |
18 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΈ = πΆ) β (πΆ β π΄) β€ (πΆ β πΈ)) |
19 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ πΈ = πΆ) β πΈ = πΆ) |
20 | 19 | oveq2d 7425 |
. . . . . . . . 9
β’ ((π β§ πΈ = πΆ) β (πΆ β πΈ) = (πΆ β πΆ)) |
21 | 18, 20 | breqtrd 5175 |
. . . . . . . 8
β’ ((π β§ πΈ = πΆ) β (πΆ β π΄) β€ (πΆ β πΆ)) |
22 | 3, 4, 5, 16, 7, 9,
11, 9, 13, 21 | legeq 27844 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β πΆ = π΄) |
23 | 3, 4, 5, 7, 9, 11,
9, 13, 15, 22 | tgcgreq 27733 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β πΆ = π΅) |
24 | | krippen.5 |
. . . . . . 7
β’ (π β π΅ = (πβπ΄)) |
25 | 24 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β π΅ = (πβπ΄)) |
26 | 23, 22, 25 | 3eqtr3rd 2782 |
. . . . 5
β’ ((π β§ πΈ = πΆ) β (πβπ΄) = π΄) |
27 | | mirval.l |
. . . . . 6
β’ πΏ = (LineGβπΊ) |
28 | | mirval.s |
. . . . . 6
β’ π = (pInvGβπΊ) |
29 | | krippen.x |
. . . . . . 7
β’ (π β π β π) |
30 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β π β π) |
31 | | krippen.m |
. . . . . 6
β’ π = (πβπ) |
32 | 3, 4, 5, 27, 28, 7, 30, 31, 11 | mirinv 27917 |
. . . . 5
β’ ((π β§ πΈ = πΆ) β ((πβπ΄) = π΄ β π = π΄)) |
33 | 26, 32 | mpbid 231 |
. . . 4
β’ ((π β§ πΈ = πΆ) β π = π΄) |
34 | | krippen.f |
. . . . . . . 8
β’ (π β πΉ β π) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β πΉ β π) |
36 | | krippen.4 |
. . . . . . . . 9
β’ (π β (πΆ β πΈ) = (πΆ β πΉ)) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΈ = πΆ) β (πΆ β πΈ) = (πΆ β πΉ)) |
38 | 37, 20 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ πΈ = πΆ) β (πΆ β πΉ) = (πΆ β πΆ)) |
39 | 3, 4, 5, 7, 9, 35,
9, 38 | axtgcgrid 27714 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β πΆ = πΉ) |
40 | | krippen.6 |
. . . . . . 7
β’ (π β πΉ = (πβπΈ)) |
41 | 40 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β πΉ = (πβπΈ)) |
42 | 19, 39, 41 | 3eqtrrd 2778 |
. . . . 5
β’ ((π β§ πΈ = πΆ) β (πβπΈ) = πΈ) |
43 | | krippen.y |
. . . . . . 7
β’ (π β π β π) |
44 | 43 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β π β π) |
45 | | krippen.n |
. . . . . 6
β’ π = (πβπ) |
46 | | krippen.e |
. . . . . . 7
β’ (π β πΈ β π) |
47 | 46 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = πΆ) β πΈ β π) |
48 | 3, 4, 5, 27, 28, 7, 44, 45, 47 | mirinv 27917 |
. . . . 5
β’ ((π β§ πΈ = πΆ) β ((πβπΈ) = πΈ β π = πΈ)) |
49 | 42, 48 | mpbid 231 |
. . . 4
β’ ((π β§ πΈ = πΆ) β π = πΈ) |
50 | 33, 49 | oveq12d 7427 |
. . 3
β’ ((π β§ πΈ = πΆ) β (ππΌπ) = (π΄πΌπΈ)) |
51 | 2, 50 | eleqtrrd 2837 |
. 2
β’ ((π β§ πΈ = πΆ) β πΆ β (ππΌπ)) |
52 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β πΆ) β πΊ β TarskiG) |
53 | 52 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β πΊ β TarskiG) |
54 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΈ β πΆ) β πΆ β π) |
55 | | eqid 2733 |
. . . . . . . 8
β’ (πβπΆ) = (πβπΆ) |
56 | 3, 4, 5, 27, 28, 52, 54, 55 | mirf 27911 |
. . . . . . 7
β’ ((π β§ πΈ β πΆ) β (πβπΆ):πβΆπ) |
57 | 43 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ β πΆ) β π β π) |
58 | 56, 57 | ffvelcdmd 7088 |
. . . . . 6
β’ ((π β§ πΈ β πΆ) β ((πβπΆ)βπ) β π) |
59 | 58 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β ((πβπΆ)βπ) β π) |
60 | | simplr 768 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π β π) |
61 | 54 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β πΆ β π) |
62 | 57 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π β π) |
63 | | simprl 770 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π β (((πβπΆ)βπ)πΌπΆ)) |
64 | 3, 4, 5, 27, 28, 6, 8, 55, 43 | mirbtwn 27909 |
. . . . . 6
β’ (π β πΆ β (((πβπΆ)βπ)πΌπ)) |
65 | 64 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β πΆ β (((πβπΆ)βπ)πΌπ)) |
66 | 3, 4, 5, 53, 59, 60, 61, 62, 63, 65 | tgbtwnexch3 27745 |
. . . 4
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β πΆ β (ππΌπ)) |
67 | 29 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π β π) |
68 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ β πΆ) β π΄ β π) |
69 | 68 | ad2antrr 725 |
. . . . . 6
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π΄ β π) |
70 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ β πΆ) β π΅ β π) |
71 | 70 | ad2antrr 725 |
. . . . . 6
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π΅ β π) |
72 | | eqid 2733 |
. . . . . . . 8
β’ (πβπ) = (πβπ) |
73 | 46 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β πΈ β π) |
74 | 56, 73 | ffvelcdmd 7088 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β ((πβπΆ)βπΈ) β π) |
75 | 34 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β πΉ β π) |
76 | 56, 75 | ffvelcdmd 7088 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β ((πβπΆ)βπΉ) β π) |
77 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β πΊ β TarskiG) |
78 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β π΄ β π) |
79 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β ((πβπΆ)βπΈ) β π) |
80 | 3, 4, 5, 77, 78, 79 | tgbtwntriv1 27742 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β π΄ β (π΄πΌ((πβπΆ)βπΈ))) |
81 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β π΄ = πΆ) |
82 | 81 | oveq1d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β (π΄πΌ((πβπΆ)βπΈ)) = (πΆπΌ((πβπΆ)βπΈ))) |
83 | 80, 82 | eleqtrd 2836 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΈ β πΆ) β§ π΄ = πΆ) β π΄ β (πΆπΌ((πβπΆ)βπΈ))) |
84 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΊ β TarskiG) |
85 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β π΄ β π) |
86 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β ((πβπΆ)βπΈ) β π) |
87 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΆ β π) |
88 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΈ β π) |
89 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΈ β πΆ) |
90 | 3, 4, 5, 6, 10, 8,
46, 1 | tgbtwncom 27739 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΆ β (πΈπΌπ΄)) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΆ β (πΈπΌπ΄)) |
92 | 3, 4, 5, 27, 28, 84, 87, 55, 88 | mirbtwn 27909 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΆ β (((πβπΆ)βπΈ)πΌπΈ)) |
93 | 3, 4, 5, 84, 86, 87, 88, 92 | tgbtwncom 27739 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β πΆ β (πΈπΌ((πβπΆ)βπΈ))) |
94 | 3, 5, 84, 88, 87, 85, 86, 89, 91, 93 | tgbtwnconn2 27827 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β (π΄ β (πΆπΌ((πβπΆ)βπΈ)) β¨ ((πβπΆ)βπΈ) β (πΆπΌπ΄))) |
95 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ πΈ β πΆ) β (πΆ β π΄) β€ (πΆ β πΈ)) |
96 | 3, 4, 5, 27, 28, 52, 54, 55, 73 | mircgr 27908 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ πΈ β πΆ) β (πΆ β ((πβπΆ)βπΈ)) = (πΆ β πΈ)) |
97 | 95, 96 | breqtrrd 5177 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ πΈ β πΆ) β (πΆ β π΄) β€ (πΆ β ((πβπΆ)βπΈ))) |
98 | 97 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β (πΆ β π΄) β€ (πΆ β ((πβπΆ)βπΈ))) |
99 | 3, 4, 5, 16, 84, 85, 86, 87, 85, 94, 98 | legbtwn 27845 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΈ β πΆ) β§ π΄ β πΆ) β π΄ β (πΆπΌ((πβπΆ)βπΈ))) |
100 | 83, 99 | pm2.61dane 3030 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β π΄ β (πΆπΌ((πβπΆ)βπΈ))) |
101 | 3, 4, 5, 52, 54, 68, 74, 100 | tgbtwncom 27739 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β π΄ β (((πβπΆ)βπΈ)πΌπΆ)) |
102 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β πΊ β TarskiG) |
103 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β π΅ β π) |
104 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β ((πβπΆ)βπΉ) β π) |
105 | 3, 4, 5, 102, 103, 104 | tgbtwntriv1 27742 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β π΅ β (π΅πΌ((πβπΆ)βπΉ))) |
106 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β π΅ = πΆ) |
107 | 106 | oveq1d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β (π΅πΌ((πβπΆ)βπΉ)) = (πΆπΌ((πβπΆ)βπΉ))) |
108 | 105, 107 | eleqtrd 2836 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΈ β πΆ) β§ π΅ = πΆ) β π΅ β (πΆπΌ((πβπΆ)βπΉ))) |
109 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΊ β TarskiG) |
110 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β π΅ β π) |
111 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β ((πβπΆ)βπΉ) β π) |
112 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΆ β π) |
113 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΉ β π) |
114 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ πΉ = πΆ) β πΊ β TarskiG) |
115 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ πΉ = πΆ) β πΆ β π) |
116 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ πΉ = πΆ) β πΈ β π) |
117 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ πΉ = πΆ) β (πΆ β πΈ) = (πΆ β πΉ)) |
118 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ πΉ = πΆ) β πΉ = πΆ) |
119 | 118 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ πΉ = πΆ) β (πΆ β πΉ) = (πΆ β πΆ)) |
120 | 117, 119 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ πΉ = πΆ) β (πΆ β πΈ) = (πΆ β πΆ)) |
121 | 3, 4, 5, 114, 115, 116, 115, 120 | axtgcgrid 27714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ πΉ = πΆ) β πΆ = πΈ) |
122 | 121 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ πΉ = πΆ) β πΈ = πΆ) |
123 | 122 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ πΈ β πΆ) β§ πΉ = πΆ) β πΈ = πΆ) |
124 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ πΈ β πΆ) β§ πΉ = πΆ) β πΈ β πΆ) |
125 | 124 | neneqd 2946 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ πΈ β πΆ) β§ πΉ = πΆ) β Β¬ πΈ = πΆ) |
126 | 123, 125 | pm2.65da 816 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ πΈ β πΆ) β Β¬ πΉ = πΆ) |
127 | 126 | neqned 2948 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ πΈ β πΆ) β πΉ β πΆ) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΉ β πΆ) |
129 | | krippen.2 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΆ β (π΅πΌπΉ)) |
130 | 3, 4, 5, 6, 12, 8,
34, 129 | tgbtwncom 27739 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΆ β (πΉπΌπ΅)) |
131 | 130 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΆ β (πΉπΌπ΅)) |
132 | 3, 4, 5, 27, 28, 109, 112, 55, 113 | mirbtwn 27909 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΆ β (((πβπΆ)βπΉ)πΌπΉ)) |
133 | 3, 4, 5, 109, 111, 112, 113, 132 | tgbtwncom 27739 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β πΆ β (πΉπΌ((πβπΆ)βπΉ))) |
134 | 3, 5, 109, 113, 112, 110, 111, 128, 131, 133 | tgbtwnconn2 27827 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β (π΅ β (πΆπΌ((πβπΆ)βπΉ)) β¨ ((πβπΆ)βπΉ) β (πΆπΌπ΅))) |
135 | 17, 14, 36 | 3brtr3d 5180 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΆ β π΅) β€ (πΆ β πΉ)) |
136 | 135 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ πΈ β πΆ) β (πΆ β π΅) β€ (πΆ β πΉ)) |
137 | 3, 4, 5, 27, 28, 52, 54, 55, 75 | mircgr 27908 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ πΈ β πΆ) β (πΆ β ((πβπΆ)βπΉ)) = (πΆ β πΉ)) |
138 | 136, 137 | breqtrrd 5177 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ πΈ β πΆ) β (πΆ β π΅) β€ (πΆ β ((πβπΆ)βπΉ))) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β (πΆ β π΅) β€ (πΆ β ((πβπΆ)βπΉ))) |
140 | 3, 4, 5, 16, 109, 110, 111, 112, 110, 134, 139 | legbtwn 27845 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΈ β πΆ) β§ π΅ β πΆ) β π΅ β (πΆπΌ((πβπΆ)βπΉ))) |
141 | 108, 140 | pm2.61dane 3030 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β π΅ β (πΆπΌ((πβπΆ)βπΉ))) |
142 | 3, 4, 5, 52, 54, 70, 76, 141 | tgbtwncom 27739 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β π΅ β (((πβπΆ)βπΉ)πΌπΆ)) |
143 | 36 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΈ β πΆ) β (πΆ β πΈ) = (πΆ β πΉ)) |
144 | 143, 96, 137 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β (πΆ β ((πβπΆ)βπΈ)) = (πΆ β ((πβπΆ)βπΉ))) |
145 | 3, 4, 5, 52, 54, 74, 54, 76, 144 | tgcgrcomlr 27731 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β (((πβπΆ)βπΈ) β πΆ) = (((πβπΆ)βπΉ) β πΆ)) |
146 | 14 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β (πΆ β π΄) = (πΆ β π΅)) |
147 | 3, 4, 5, 52, 54, 68, 54, 70, 146 | tgcgrcomlr 27731 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β (π΄ β πΆ) = (π΅ β πΆ)) |
148 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (πβ((πβπΆ)βπ)) = (πβ((πβπΆ)βπ)) |
149 | 3, 4, 5, 27, 28, 52, 58, 148, 74 | mircgr 27908 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΈ β πΆ) β (((πβπΆ)βπ) β ((πβ((πβπΆ)βπ))β((πβπΆ)βπΈ))) = (((πβπΆ)βπ) β ((πβπΆ)βπΈ))) |
150 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπΆ)βπ) = ((πβπΆ)βπ) |
151 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπΆ)βπΈ) = ((πβπΆ)βπΈ) |
152 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπΆ)βπΉ) = ((πβπΆ)βπΉ) |
153 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ πΈ β πΆ) β πΉ = (πβπΈ)) |
154 | 45 | fveq1i 6893 |
. . . . . . . . . . . . . . . . . . 19
β’ (πβπΈ) = ((πβπ)βπΈ) |
155 | 153, 154 | eqtr2di 2790 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ πΈ β πΆ) β ((πβπ)βπΈ) = πΉ) |
156 | 3, 4, 5, 27, 28, 52, 55, 150, 151, 152, 54, 57, 73, 75, 155 | mirauto 27935 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ πΈ β πΆ) β ((πβ((πβπΆ)βπ))β((πβπΆ)βπΈ)) = ((πβπΆ)βπΉ)) |
157 | 156 | oveq2d 7425 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΈ β πΆ) β (((πβπΆ)βπ) β ((πβ((πβπΆ)βπ))β((πβπΆ)βπΈ))) = (((πβπΆ)βπ) β ((πβπΆ)βπΉ))) |
158 | 149, 157 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΈ β πΆ) β (((πβπΆ)βπ) β ((πβπΆ)βπΈ)) = (((πβπΆ)βπ) β ((πβπΆ)βπΉ))) |
159 | 3, 4, 5, 52, 58, 74, 58, 76, 158 | tgcgrcomlr 27731 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β (((πβπΆ)βπΈ) β ((πβπΆ)βπ)) = (((πβπΆ)βπΉ) β ((πβπΆ)βπ))) |
160 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΈ β πΆ) β (πΆ β ((πβπΆ)βπ)) = (πΆ β ((πβπΆ)βπ))) |
161 | 3, 4, 5, 52, 74, 68, 54, 58, 76, 70, 54, 58, 101, 142, 145, 147, 159, 160 | tgifscgr 27759 |
. . . . . . . . . . . . 13
β’ ((π β§ πΈ β πΆ) β (π΄ β ((πβπΆ)βπ)) = (π΅ β ((πβπΆ)βπ))) |
162 | 3, 4, 5, 52, 68, 58, 70, 58, 161 | tgcgrcomlr 27731 |
. . . . . . . . . . . 12
β’ ((π β§ πΈ β πΆ) β (((πβπΆ)βπ) β π΄) = (((πβπΆ)βπ) β π΅)) |
163 | 162 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β (((πβπΆ)βπ) β π΄) = (((πβπΆ)βπ) β π΅)) |
164 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β πΊ β TarskiG) |
165 | 59 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β ((πβπΆ)βπ) β π) |
166 | 60 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β π β π) |
167 | 63 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β π β (((πβπΆ)βπ)πΌπΆ)) |
168 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β ((πβπΆ)βπ) = πΆ) |
169 | 168 | oveq2d 7425 |
. . . . . . . . . . . . . 14
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β (((πβπΆ)βπ)πΌ((πβπΆ)βπ)) = (((πβπΆ)βπ)πΌπΆ)) |
170 | 167, 169 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β π β (((πβπΆ)βπ)πΌ((πβπΆ)βπ))) |
171 | 3, 4, 5, 164, 165, 166, 170 | axtgbtwnid 27717 |
. . . . . . . . . . . 12
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β ((πβπΆ)βπ) = π) |
172 | 171 | oveq1d 7424 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β (((πβπΆ)βπ) β π΄) = (π β π΄)) |
173 | 171 | oveq1d 7424 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β (((πβπΆ)βπ) β π΅) = (π β π΅)) |
174 | 163, 172,
173 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) = πΆ) β (π β π΄) = (π β π΅)) |
175 | 52 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β πΊ β TarskiG) |
176 | 58 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β ((πβπΆ)βπ) β π) |
177 | 54 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β πΆ β π) |
178 | 60 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β π β π) |
179 | | eqid 2733 |
. . . . . . . . . . 11
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
180 | 68 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β π΄ β π) |
181 | 70 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β π΅ β π) |
182 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β ((πβπΆ)βπ) β πΆ) |
183 | 59 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β ((πβπΆ)βπ) β π) |
184 | 63 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β π β (((πβπΆ)βπ)πΌπΆ)) |
185 | 3, 27, 5, 175, 183, 178, 177, 184 | btwncolg3 27808 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β (πΆ β (((πβπΆ)βπ)πΏπ) β¨ ((πβπΆ)βπ) = π)) |
186 | 162 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β (((πβπΆ)βπ) β π΄) = (((πβπΆ)βπ) β π΅)) |
187 | 146 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β (πΆ β π΄) = (πΆ β π΅)) |
188 | 3, 27, 5, 175, 176, 177, 178, 179, 180, 181, 4, 182, 185, 186, 187 | lncgr 27820 |
. . . . . . . . . 10
β’
(((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β§ ((πβπΆ)βπ) β πΆ) β (π β π΄) = (π β π΅)) |
189 | 174, 188 | pm2.61dane 3030 |
. . . . . . . . 9
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β (π β π΄) = (π β π΅)) |
190 | 189 | eqcomd 2739 |
. . . . . . . 8
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β (π β π΅) = (π β π΄)) |
191 | | simprr 772 |
. . . . . . . . 9
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π β (π΄πΌπ΅)) |
192 | 3, 4, 5, 53, 69, 60, 71, 191 | tgbtwncom 27739 |
. . . . . . . 8
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π β (π΅πΌπ΄)) |
193 | 3, 4, 5, 27, 28, 53, 60, 72, 69, 71, 190, 192 | ismir 27910 |
. . . . . . 7
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π΅ = ((πβπ)βπ΄)) |
194 | 193 | eqcomd 2739 |
. . . . . 6
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β ((πβπ)βπ΄) = π΅) |
195 | 24 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π΅ = (πβπ΄)) |
196 | 31 | fveq1i 6893 |
. . . . . . 7
β’ (πβπ΄) = ((πβπ)βπ΄) |
197 | 195, 196 | eqtr2di 2790 |
. . . . . 6
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β ((πβπ)βπ΄) = π΅) |
198 | 3, 4, 5, 27, 28, 53, 60, 67, 69, 71, 194, 197 | miduniq 27936 |
. . . . 5
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β π = π) |
199 | 198 | oveq1d 7424 |
. . . 4
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β (ππΌπ) = (ππΌπ)) |
200 | 66, 199 | eleqtrd 2836 |
. . 3
β’ ((((π β§ πΈ β πΆ) β§ π β π) β§ (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) β πΆ β (ππΌπ)) |
201 | 3, 4, 5, 27, 28, 52, 57, 45, 73 | mirbtwn 27909 |
. . . . . . 7
β’ ((π β§ πΈ β πΆ) β π β ((πβπΈ)πΌπΈ)) |
202 | 153 | oveq1d 7424 |
. . . . . . 7
β’ ((π β§ πΈ β πΆ) β (πΉπΌπΈ) = ((πβπΈ)πΌπΈ)) |
203 | 201, 202 | eleqtrrd 2837 |
. . . . . 6
β’ ((π β§ πΈ β πΆ) β π β (πΉπΌπΈ)) |
204 | 3, 4, 5, 52, 75, 57, 73, 203 | tgbtwncom 27739 |
. . . . 5
β’ ((π β§ πΈ β πΆ) β π β (πΈπΌπΉ)) |
205 | 3, 4, 5, 27, 28, 52, 54, 55, 73, 57, 75, 204 | mirbtwni 27922 |
. . . 4
β’ ((π β§ πΈ β πΆ) β ((πβπΆ)βπ) β (((πβπΆ)βπΈ)πΌ((πβπΆ)βπΉ))) |
206 | 3, 4, 5, 52, 74, 68, 54, 76, 70, 58, 101, 142, 205 | tgtrisegint 27750 |
. . 3
β’ ((π β§ πΈ β πΆ) β βπ β π (π β (((πβπΆ)βπ)πΌπΆ) β§ π β (π΄πΌπ΅))) |
207 | 200, 206 | r19.29a 3163 |
. 2
β’ ((π β§ πΈ β πΆ) β πΆ β (ππΌπ)) |
208 | 51, 207 | pm2.61dane 3030 |
1
β’ (π β πΆ β (ππΌπ)) |