Step | Hyp | Ref
| Expression |
1 | | tgbtwndiff.p |
. . . 4
β’ π = (BaseβπΊ) |
2 | | tgbtwndiff.d |
. . . 4
β’ β =
(distβπΊ) |
3 | | tgbtwndiff.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
4 | | tgbtwndiff.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
5 | 4 | ad3antrrr 727 |
. . . 4
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β πΊ β TarskiG) |
6 | | tgbtwndiff.a |
. . . . 5
β’ (π β π΄ β π) |
7 | 6 | ad3antrrr 727 |
. . . 4
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β π΄ β π) |
8 | | tgbtwndiff.b |
. . . . 5
β’ (π β π΅ β π) |
9 | 8 | ad3antrrr 727 |
. . . 4
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β π΅ β π) |
10 | | simpllr 773 |
. . . 4
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β π’ β π) |
11 | | simplr 766 |
. . . 4
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β π£ β π) |
12 | 1, 2, 3, 5, 7, 9, 10, 11 | axtgsegcon 27979 |
. . 3
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β βπ β π (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π’ β π£))) |
13 | 5 | ad3antrrr 727 |
. . . . . . . . 9
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β πΊ β TarskiG) |
14 | 10 | ad3antrrr 727 |
. . . . . . . . 9
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β π’ β π) |
15 | 11 | ad3antrrr 727 |
. . . . . . . . 9
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β π£ β π) |
16 | 9 | ad3antrrr 727 |
. . . . . . . . 9
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β π΅ β π) |
17 | | simpr 484 |
. . . . . . . . . . 11
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β π΅ = π) |
18 | 17 | oveq2d 7428 |
. . . . . . . . . 10
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β (π΅ β π΅) = (π΅ β π)) |
19 | | simplr 766 |
. . . . . . . . . 10
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β (π΅ β π) = (π’ β π£)) |
20 | 18, 19 | eqtr2d 2772 |
. . . . . . . . 9
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β (π’ β π£) = (π΅ β π΅)) |
21 | 1, 2, 3, 13, 14, 15, 16, 20 | axtgcgrid 27978 |
. . . . . . . 8
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β π’ = π£) |
22 | | simp-4r 781 |
. . . . . . . . 9
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β π’ β π£) |
23 | 22 | neneqd 2944 |
. . . . . . . 8
β’
(((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β§ π΅ = π) β Β¬ π’ = π£) |
24 | 21, 23 | pm2.65da 814 |
. . . . . . 7
β’
((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β Β¬ π΅ = π) |
25 | 24 | neqned 2946 |
. . . . . 6
β’
((((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β§ (π΅ β π) = (π’ β π£)) β π΅ β π) |
26 | 25 | ex 412 |
. . . . 5
β’
(((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β ((π΅ β π) = (π’ β π£) β π΅ β π)) |
27 | 26 | anim2d 611 |
. . . 4
β’
(((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β§ π β π) β ((π΅ β (π΄πΌπ) β§ (π΅ β π) = (π’ β π£)) β (π΅ β (π΄πΌπ) β§ π΅ β π))) |
28 | 27 | reximdva 3167 |
. . 3
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β (βπ β π (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π’ β π£)) β βπ β π (π΅ β (π΄πΌπ) β§ π΅ β π))) |
29 | 12, 28 | mpd 15 |
. 2
β’ ((((π β§ π’ β π) β§ π£ β π) β§ π’ β π£) β βπ β π (π΅ β (π΄πΌπ) β§ π΅ β π)) |
30 | | tgbtwndiff.l |
. . 3
β’ (π β 2 β€
(β―βπ)) |
31 | 1, 2, 3, 4, 30 | tglowdim1 28015 |
. 2
β’ (π β βπ’ β π βπ£ β π π’ β π£) |
32 | 29, 31 | r19.29vva 3212 |
1
β’ (π β βπ β π (π΅ β (π΄πΌπ) β§ π΅ β π)) |