Step |
Hyp |
Ref |
Expression |
1 |
|
dih1dimat.h |
|
2 |
|
dih1dimat.u |
|
3 |
|
dih1dimat.i |
|
4 |
|
dih1dimat.a |
|
5 |
|
dih1dimat.b |
|
6 |
|
dih1dimat.l |
|
7 |
|
dih1dimat.c |
|
8 |
|
dih1dimat.p |
|
9 |
|
dih1dimat.t |
|
10 |
|
dih1dimat.r |
|
11 |
|
dih1dimat.e |
|
12 |
|
dih1dimat.o |
|
13 |
|
dih1dimat.d |
|
14 |
|
dih1dimat.j |
|
15 |
|
dih1dimat.v |
|
16 |
|
dih1dimat.m |
|
17 |
|
dih1dimat.s |
|
18 |
|
dih1dimat.n |
|
19 |
|
dih1dimat.z |
|
20 |
|
dih1dimat.g |
|
21 |
|
id |
|
22 |
1 2 21
|
dvhlvec |
|
23 |
15 18 19 4
|
islsat |
|
24 |
22 23
|
syl |
|
25 |
24
|
biimpa |
|
26 |
|
eldifi |
|
27 |
1 9 11 2 15
|
dvhvbase |
|
28 |
27
|
eleq2d |
|
29 |
26 28
|
syl5ib |
|
30 |
29
|
imp |
|
31 |
|
simpr |
|
32 |
31
|
opeq2d |
|
33 |
32
|
sneqd |
|
34 |
33
|
fveq2d |
|
35 |
|
simpl |
|
36 |
5 1 9 10
|
trlcl |
|
37 |
6 1 9 10
|
trlle |
|
38 |
|
eqid |
|
39 |
5 6 1 3 38
|
dihvalb |
|
40 |
35 36 37 39
|
syl12anc |
|
41 |
5 1 9 10 12 2 38 18
|
dib1dim2 |
|
42 |
40 41
|
eqtr2d |
|
43 |
5 1 3 2 17
|
dihf11 |
|
44 |
43
|
adantr |
|
45 |
|
f1fn |
|
46 |
44 45
|
syl |
|
47 |
|
fnfvelrn |
|
48 |
46 36 47
|
syl2anc |
|
49 |
42 48
|
eqeltrd |
|
50 |
49
|
adantrr |
|
51 |
50
|
adantr |
|
52 |
34 51
|
eqeltrd |
|
53 |
|
simpll |
|
54 |
|
eqid |
|
55 |
1 11 2 13 54
|
dvhbase |
|
56 |
53 55
|
syl |
|
57 |
56
|
rexeqdv |
|
58 |
|
simplll |
|
59 |
|
simpr |
|
60 |
|
opelxpi |
|
61 |
60
|
ad3antlr |
|
62 |
1 9 11 2 16
|
dvhvscacl |
|
63 |
58 59 61 62
|
syl12anc |
|
64 |
|
eleq1a |
|
65 |
63 64
|
syl |
|
66 |
65
|
rexlimdva |
|
67 |
66
|
pm4.71rd |
|
68 |
|
simplrl |
|
69 |
68
|
adantr |
|
70 |
|
simplrr |
|
71 |
70
|
adantr |
|
72 |
1 9 11 2 16
|
dvhopvsca |
|
73 |
58 59 69 71 72
|
syl13anc |
|
74 |
73
|
eqeq2d |
|
75 |
74
|
rexbidva |
|
76 |
75
|
anbi2d |
|
77 |
57 67 76
|
3bitrd |
|
78 |
77
|
abbidv |
|
79 |
|
df-rab |
|
80 |
78 79
|
eqtr4di |
|
81 |
|
ssrab2 |
|
82 |
|
relxp |
|
83 |
|
relss |
|
84 |
81 82 83
|
mp2 |
|
85 |
|
relopab |
|
86 |
|
vex |
|
87 |
|
vex |
|
88 |
|
eqeq1 |
|
89 |
88
|
anbi1d |
|
90 |
|
fveq1 |
|
91 |
90
|
eqeq2d |
|
92 |
|
eleq1w |
|
93 |
91 92
|
anbi12d |
|
94 |
86 87 89 93
|
opelopab |
|
95 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
|
dih1dimatlem0 |
|
96 |
95
|
3expa |
|
97 |
|
opelxp |
|
98 |
86 87
|
opth |
|
99 |
98
|
rexbii |
|
100 |
97 99
|
anbi12i |
|
101 |
96 100
|
bitr4di |
|
102 |
|
eqeq1 |
|
103 |
102
|
rexbidv |
|
104 |
103
|
elrab |
|
105 |
101 104
|
bitr4di |
|
106 |
94 105
|
syl5rbb |
|
107 |
84 85 106
|
eqrelrdv |
|
108 |
80 107
|
eqtrd |
|
109 |
1 2 53
|
dvhlmod |
|
110 |
1 9 11 2 15
|
dvhelvbasei |
|
111 |
110
|
adantr |
|
112 |
13 54 15 16 18
|
lspsn |
|
113 |
109 111 112
|
syl2anc |
|
114 |
|
simpr |
|
115 |
5 1 9 11 12 2 13 14
|
tendoinvcl |
|
116 |
115
|
simpld |
|
117 |
53 70 114 116
|
syl3anc |
|
118 |
1 9 11
|
tendocl |
|
119 |
53 117 68 118
|
syl3anc |
|
120 |
6 7 1 8
|
lhpocnel2 |
|
121 |
53 120
|
syl |
|
122 |
6 7 1 9
|
ltrnel |
|
123 |
53 119 121 122
|
syl3anc |
|
124 |
|
eqid |
|
125 |
6 7 1 124 3
|
dihvalcqat |
|
126 |
53 123 125
|
syl2anc |
|
127 |
6 7 1 8 9 11 124 20
|
dicval2 |
|
128 |
53 123 127
|
syl2anc |
|
129 |
126 128
|
eqtrd |
|
130 |
108 113 129
|
3eqtr4d |
|
131 |
5 1 3
|
dihfn |
|
132 |
131
|
adantr |
|
133 |
132
|
adantr |
|
134 |
|
simplll |
|
135 |
|
hlop |
|
136 |
134 135
|
syl |
|
137 |
5 1
|
lhpbase |
|
138 |
137
|
ad3antlr |
|
139 |
|
eqid |
|
140 |
5 139
|
opoccl |
|
141 |
136 138 140
|
syl2anc |
|
142 |
8 141
|
eqeltrid |
|
143 |
5 1 9
|
ltrncl |
|
144 |
53 119 142 143
|
syl3anc |
|
145 |
|
fnfvelrn |
|
146 |
133 144 145
|
syl2anc |
|
147 |
130 146
|
eqeltrd |
|
148 |
52 147
|
pm2.61dane |
|
149 |
148
|
ralrimivva |
|
150 |
|
sneq |
|
151 |
150
|
fveq2d |
|
152 |
151
|
eleq1d |
|
153 |
152
|
ralxp |
|
154 |
149 153
|
sylibr |
|
155 |
154
|
r19.21bi |
|
156 |
30 155
|
syldan |
|
157 |
|
eleq1a |
|
158 |
156 157
|
syl |
|
159 |
158
|
rexlimdva |
|
160 |
159
|
adantr |
|
161 |
25 160
|
mpd |
|