Step |
Hyp |
Ref |
Expression |
1 |
|
trgcopy.p |
|
2 |
|
trgcopy.m |
|
3 |
|
trgcopy.i |
|
4 |
|
trgcopy.l |
|
5 |
|
trgcopy.k |
|
6 |
|
trgcopy.g |
|
7 |
|
trgcopy.a |
|
8 |
|
trgcopy.b |
|
9 |
|
trgcopy.c |
|
10 |
|
trgcopy.d |
|
11 |
|
trgcopy.e |
|
12 |
|
trgcopy.f |
|
13 |
|
trgcopy.1 |
|
14 |
|
trgcopy.2 |
|
15 |
|
trgcopy.3 |
|
16 |
|
trgcopyeulem.o |
|
17 |
|
trgcopyeulem.x |
|
18 |
|
trgcopyeulem.y |
|
19 |
|
trgcopyeulem.1 |
|
20 |
|
trgcopyeulem.2 |
|
21 |
|
trgcopyeulem.3 |
|
22 |
|
trgcopyeulem.4 |
|
23 |
1 4 3 6 8 9 7 13
|
ncoltgdim2 |
|
24 |
|
eqid |
|
25 |
1 3 4 6 10 11 12 14
|
ncolne1 |
|
26 |
1 3 4 6 10 11 25
|
tgelrnln |
|
27 |
|
eqid |
|
28 |
6
|
ad2antrr |
|
29 |
26
|
ad2antrr |
|
30 |
|
simplr |
|
31 |
1 4 3 28 29 30
|
tglnpt |
|
32 |
|
eqid |
|
33 |
1 2 3 6 23 24 4 26 18
|
lmicl |
|
34 |
33
|
ad2antrr |
|
35 |
17
|
ad2antrr |
|
36 |
10
|
ad2antrr |
|
37 |
11
|
ad2antrr |
|
38 |
|
eqid |
|
39 |
25
|
ad2antrr |
|
40 |
39
|
necomd |
|
41 |
1 3 4 28 37 36 31 40 30
|
lncom |
|
42 |
41
|
orcd |
|
43 |
1 4 3 28 37 36 31 42
|
colrot1 |
|
44 |
1 2 3 38 6 7 8 9 10 11 17 19
|
cgr3simp3 |
|
45 |
1 2 3 6 9 7 17 10 44
|
tgcgrcomlr |
|
46 |
1 2 3 38 6 7 8 9 10 11 18 20
|
cgr3simp3 |
|
47 |
1 2 3 6 9 7 18 10 46
|
tgcgrcomlr |
|
48 |
45 47
|
eqtr3d |
|
49 |
1 2 3 6 23 24 4 26 10 18
|
lmiiso |
|
50 |
1 3 4 6 10 11 25
|
tglinerflx1 |
|
51 |
1 2 3 6 23 24 4 26 10 50
|
lmicinv |
|
52 |
51
|
oveq1d |
|
53 |
48 49 52
|
3eqtr2d |
|
54 |
53
|
ad2antrr |
|
55 |
1 2 3 38 6 7 8 9 10 11 17 19
|
cgr3simp2 |
|
56 |
1 2 3 38 6 7 8 9 10 11 18 20
|
cgr3simp2 |
|
57 |
55 56
|
eqtr3d |
|
58 |
1 2 3 6 23 24 4 26 11 18
|
lmiiso |
|
59 |
1 3 4 6 10 11 25
|
tglinerflx2 |
|
60 |
1 2 3 6 23 24 4 26 11 59
|
lmicinv |
|
61 |
60
|
oveq1d |
|
62 |
57 58 61
|
3eqtr2d |
|
63 |
62
|
ad2antrr |
|
64 |
1 4 3 28 36 37 31 38 35 34 2 39 43 54 63
|
lncgr |
|
65 |
|
simpr |
|
66 |
1 2 3 4 27 28 31 32 34 35 64 65
|
ismir |
|
67 |
66
|
eqcomd |
|
68 |
1 2 3 4 27 28 31 32 34 67
|
mircom |
|
69 |
68
|
eqcomd |
|
70 |
23
|
ad2antrr |
|
71 |
1 2 3 28 70 35 34 27 31
|
ismidb |
|
72 |
69 71
|
mpbid |
|
73 |
72 30
|
eqeltrd |
|
74 |
1 3 4 6 26 17 16 12 21
|
hpgcom |
|
75 |
1 3 4 6 26 18 16 12 22 17 74
|
hpgtr |
|
76 |
1 3 4 16 6 26 18 12 22
|
hpgne1 |
|
77 |
1 2 3 4 6 23 26 16 24 18 76
|
lmiopp |
|
78 |
1 3 4 16 6 26 18 17 33 77
|
lnopp2hpgb |
|
79 |
75 78
|
mpbird |
|
80 |
1 2 3 16 17 33
|
islnopp |
|
81 |
79 80
|
mpbid |
|
82 |
81
|
simprd |
|
83 |
73 82
|
r19.29a |
|
84 |
28
|
adantr |
|
85 |
29
|
adantr |
|
86 |
1 2 3 16 4 26 6 17 33 79
|
oppne3 |
|
87 |
1 3 4 6 17 33 86
|
tgelrnln |
|
88 |
87
|
ad2antrr |
|
89 |
88
|
adantr |
|
90 |
86
|
ad2antrr |
|
91 |
1 3 4 28 35 34 31 90 65
|
btwnlng1 |
|
92 |
30 91
|
elind |
|
93 |
92
|
adantr |
|
94 |
59
|
ad3antrrr |
|
95 |
1 3 4 6 17 33 86
|
tglinerflx1 |
|
96 |
95
|
ad3antrrr |
|
97 |
|
simpr |
|
98 |
81
|
simplld |
|
99 |
98
|
ad2antrr |
|
100 |
|
nelne2 |
|
101 |
30 99 100
|
syl2anc |
|
102 |
101
|
necomd |
|
103 |
102
|
adantr |
|
104 |
69
|
oveq2d |
|
105 |
63 104
|
eqtrd |
|
106 |
105
|
adantr |
|
107 |
37
|
adantr |
|
108 |
31
|
adantr |
|
109 |
35
|
adantr |
|
110 |
1 2 3 4 27 84 107 108 109
|
israg |
|
111 |
106 110
|
mpbird |
|
112 |
1 2 3 4 84 85 89 93 94 96 97 103 111
|
ragperp |
|
113 |
28
|
adantr |
|
114 |
29
|
adantr |
|
115 |
88
|
adantr |
|
116 |
92
|
adantr |
|
117 |
50
|
ad3antrrr |
|
118 |
95
|
ad3antrrr |
|
119 |
|
simpr |
|
120 |
102
|
adantr |
|
121 |
69
|
oveq2d |
|
122 |
54 121
|
eqtrd |
|
123 |
122
|
adantr |
|
124 |
36
|
adantr |
|
125 |
31
|
adantr |
|
126 |
35
|
adantr |
|
127 |
1 2 3 4 27 113 124 125 126
|
israg |
|
128 |
123 127
|
mpbird |
|
129 |
1 2 3 4 113 114 115 116 117 118 119 120 128
|
ragperp |
|
130 |
|
neneor |
|
131 |
40 130
|
syl |
|
132 |
112 129 131
|
mpjaodan |
|
133 |
132
|
orcd |
|
134 |
133 82
|
r19.29a |
|
135 |
1 2 3 6 23 24 4 26 17 33
|
islmib |
|
136 |
83 134 135
|
mpbir2and |
|
137 |
136
|
eqcomd |
|
138 |
1 2 3 6 23 24 4 26 17 18 137
|
lmieq |
|