Step | Hyp | Ref
| Expression |
1 | | symquadlem.1 |
. . . . . . . 8
|
2 | | mirval.p |
. . . . . . . . . . 11
|
3 | | mirval.l |
. . . . . . . . . . 11
LineG |
4 | | mirval.i |
. . . . . . . . . . 11
Itv |
5 | | mirval.g |
. . . . . . . . . . 11
TarskiG |
6 | | symquadlem.b |
. . . . . . . . . . 11
|
7 | | symquadlem.a |
. . . . . . . . . . 11
|
8 | | mirval.d |
. . . . . . . . . . . 12
|
9 | 2, 8, 4, 5, 6, 7 | tgbtwntriv2 25382 |
. . . . . . . . . . 11
|
10 | 2, 3, 4, 5, 6, 7, 7, 9 | btwncolg1 25450 |
. . . . . . . . . 10
|
11 | 10 | adantr 481 |
. . . . . . . . 9
|
12 | | simpr 477 |
. . . . . . . . . . . 12
|
13 | 12 | oveq2d 6666 |
. . . . . . . . . . 11
|
14 | 13 | eleq2d 2687 |
. . . . . . . . . 10
|
15 | 12 | eqeq2d 2632 |
. . . . . . . . . 10
|
16 | 14, 15 | orbi12d 746 |
. . . . . . . . 9
|
17 | 11, 16 | mpbid 222 |
. . . . . . . 8
|
18 | 1, 17 | mtand 691 |
. . . . . . 7
|
19 | 18 | neqned 2801 |
. . . . . 6
|
20 | 19 | ad2antrr 762 |
. . . . 5
cgrG |
21 | 20 | necomd 2849 |
. . . 4
cgrG |
22 | 21 | neneqd 2799 |
. . 3
cgrG
|
23 | | mirval.s |
. . . . . 6
pInvG |
24 | 5 | ad2antrr 762 |
. . . . . 6
cgrG
TarskiG |
25 | | symquadlem.m |
. . . . . 6
|
26 | | symquadlem.c |
. . . . . . 7
|
27 | 26 | ad2antrr 762 |
. . . . . 6
cgrG
|
28 | 7 | ad2antrr 762 |
. . . . . 6
cgrG
|
29 | | symquadlem.x |
. . . . . . 7
|
30 | 29 | ad2antrr 762 |
. . . . . 6
cgrG
|
31 | | symquadlem.5 |
. . . . . . . 8
|
32 | 31 | ad2antrr 762 |
. . . . . . 7
cgrG |
33 | 2, 3, 4, 24, 28, 27, 30, 32 | colcom 25453 |
. . . . . 6
cgrG |
34 | 6 | ad2antrr 762 |
. . . . . . . 8
cgrG
|
35 | | symquadlem.d |
. . . . . . . . 9
|
36 | 35 | ad2antrr 762 |
. . . . . . . 8
cgrG
|
37 | | eqid 2622 |
. . . . . . . 8
cgrG cgrG |
38 | | simplr 792 |
. . . . . . . 8
cgrG
|
39 | | symquadlem.6 |
. . . . . . . . . . 11
|
40 | 2, 3, 4, 5, 6, 35,
29, 39 | colrot2 25455 |
. . . . . . . . . 10
|
41 | 2, 3, 4, 5, 29, 6,
35, 40 | colcom 25453 |
. . . . . . . . 9
|
42 | 41 | ad2antrr 762 |
. . . . . . . 8
cgrG |
43 | | simpr 477 |
. . . . . . . 8
cgrG cgrG |
44 | | symquadlem.4 |
. . . . . . . . 9
|
45 | 44 | ad2antrr 762 |
. . . . . . . 8
cgrG |
46 | | symquadlem.3 |
. . . . . . . . . . 11
|
47 | 2, 8, 4, 5, 7, 6, 26, 35, 46 | tgcgrcomlr 25375 |
. . . . . . . . . 10
|
48 | 47 | ad2antrr 762 |
. . . . . . . . 9
cgrG |
49 | 48 | eqcomd 2628 |
. . . . . . . 8
cgrG |
50 | | symquadlem.2 |
. . . . . . . . 9
|
51 | 50 | ad2antrr 762 |
. . . . . . . 8
cgrG |
52 | 2, 3, 4, 24, 34, 36, 30, 37, 36, 34, 8, 27, 38, 28, 42, 43, 45, 49, 51 | tgfscgr 25463 |
. . . . . . 7
cgrG |
53 | 2, 3, 4, 5, 6, 26,
7, 1 | ncolcom 25456 |
. . . . . . . . . 10
|
54 | 53 | ad2antrr 762 |
. . . . . . . . 9
cgrG |
55 | 31 | orcomd 403 |
. . . . . . . . . . . 12
|
56 | 55 | ord 392 |
. . . . . . . . . . 11
|
57 | 18, 56 | mpd 15 |
. . . . . . . . . 10
|
58 | 57 | ad2antrr 762 |
. . . . . . . . 9
cgrG
|
59 | 18 | ad2antrr 762 |
. . . . . . . . . 10
cgrG
|
60 | 45 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
cgrG |
61 | 2, 3, 4, 24, 34, 36, 30, 37, 36, 34, 8, 28, 38, 27, 42, 43, 48, 60, 51 | tgfscgr 25463 |
. . . . . . . . . . . . . . . 16
cgrG |
62 | 2, 8, 4, 24, 30, 28, 38, 27, 61 | tgcgrcomlr 25375 |
. . . . . . . . . . . . . . 15
cgrG |
63 | 2, 8, 4, 24, 27, 28 | axtgcgrrflx 25361 |
. . . . . . . . . . . . . . 15
cgrG |
64 | 2, 8, 37, 24, 28, 30, 27, 27, 38, 28, 62, 52, 63 | trgcgr 25411 |
. . . . . . . . . . . . . 14
cgrG cgrG |
65 | 2, 3, 4, 24, 28, 30, 27, 37, 27, 38, 28, 32, 64 | lnxfr 25461 |
. . . . . . . . . . . . 13
cgrG |
66 | 2, 3, 4, 24, 27, 28, 38, 65 | colcom 25453 |
. . . . . . . . . . . 12
cgrG |
67 | 66 | orcomd 403 |
. . . . . . . . . . 11
cgrG |
68 | 67 | ord 392 |
. . . . . . . . . 10
cgrG
|
69 | 59, 68 | mpd 15 |
. . . . . . . . 9
cgrG
|
70 | 50 | neneqd 2799 |
. . . . . . . . . . 11
|
71 | 39 | orcomd 403 |
. . . . . . . . . . . 12
|
72 | 71 | ord 392 |
. . . . . . . . . . 11
|
73 | 70, 72 | mpd 15 |
. . . . . . . . . 10
|
74 | 73 | ad2antrr 762 |
. . . . . . . . 9
cgrG
|
75 | 70 | ad2antrr 762 |
. . . . . . . . . 10
cgrG
|
76 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . 14
cgrG |
77 | 2, 8, 4, 37, 24, 34, 36, 30, 36, 34, 38, 43 | cgr3swap23 25419 |
. . . . . . . . . . . . . 14
cgrG cgrG |
78 | 2, 3, 4, 24, 34, 30, 36, 37, 36, 38, 34, 76, 77 | lnxfr 25461 |
. . . . . . . . . . . . 13
cgrG |
79 | 2, 3, 4, 24, 36, 34, 38, 78 | colcom 25453 |
. . . . . . . . . . . 12
cgrG |
80 | 79 | orcomd 403 |
. . . . . . . . . . 11
cgrG |
81 | 80 | ord 392 |
. . . . . . . . . 10
cgrG
|
82 | 75, 81 | mpd 15 |
. . . . . . . . 9
cgrG
|
83 | 2, 4, 3, 24, 28, 27, 34, 36, 54, 58, 69, 74, 82 | tglineinteq 25540 |
. . . . . . . 8
cgrG
|
84 | 83 | oveq1d 6665 |
. . . . . . 7
cgrG |
85 | 52, 84 | eqtr4d 2659 |
. . . . . 6
cgrG |
86 | 2, 8, 4, 3, 23, 24, 25, 27, 28, 30, 33, 85 | colmid 25583 |
. . . . 5
cgrG |
87 | 86 | orcomd 403 |
. . . 4
cgrG |
88 | 87 | ord 392 |
. . 3
cgrG
|
89 | 22, 88 | mpd 15 |
. 2
cgrG
|
90 | 2, 8, 4, 5, 6, 35 | axtgcgrrflx 25361 |
. . 3
|
91 | 2, 3, 4, 5, 6, 35,
29, 37, 35, 6, 8, 41, 90 | lnext 25462 |
. 2
cgrG |
92 | 89, 91 | r19.29a 3078 |
1
|