Step | Hyp | Ref
| Expression |
1 | | dih1dimat.h |
. . . . 5
|
2 | | dih1dimat.u |
. . . . 5
|
3 | | id 22 |
. . . . 5
|
4 | 1, 2, 3 | dvhlvec 36398 |
. . . 4
|
5 | | dih1dimat.v |
. . . . 5
|
6 | | dih1dimat.n |
. . . . 5
|
7 | | dih1dimat.z |
. . . . 5
|
8 | | dih1dimat.a |
. . . . 5
LSAtoms |
9 | 5, 6, 7, 8 | islsat 34278 |
. . . 4
|
10 | 4, 9 | syl 17 |
. . 3
|
11 | 10 | biimpa 501 |
. 2
|
12 | | eldifi 3732 |
. . . . . . . 8
|
13 | | dih1dimat.t |
. . . . . . . . . 10
|
14 | | dih1dimat.e |
. . . . . . . . . 10
|
15 | 1, 13, 14, 2, 5 | dvhvbase 36376 |
. . . . . . . . 9
|
16 | 15 | eleq2d 2687 |
. . . . . . . 8
|
17 | 12, 16 | syl5ib 234 |
. . . . . . 7
|
18 | 17 | imp 445 |
. . . . . 6
|
19 | | simpr 477 |
. . . . . . . . . . . . . 14
|
20 | 19 | opeq2d 4409 |
. . . . . . . . . . . . 13
|
21 | 20 | sneqd 4189 |
. . . . . . . . . . . 12
|
22 | 21 | fveq2d 6195 |
. . . . . . . . . . 11
|
23 | | simpl 473 |
. . . . . . . . . . . . . . . 16
|
24 | | dih1dimat.b |
. . . . . . . . . . . . . . . . 17
|
25 | | dih1dimat.r |
. . . . . . . . . . . . . . . . 17
|
26 | 24, 1, 13, 25 | trlcl 35451 |
. . . . . . . . . . . . . . . 16
|
27 | | dih1dimat.l |
. . . . . . . . . . . . . . . . 17
|
28 | 27, 1, 13, 25 | trlle 35471 |
. . . . . . . . . . . . . . . 16
|
29 | | dih1dimat.i |
. . . . . . . . . . . . . . . . 17
|
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
31 | 24, 27, 1, 29, 30 | dihvalb 36526 |
. . . . . . . . . . . . . . . 16
|
32 | 23, 26, 28, 31 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
|
33 | | dih1dimat.o |
. . . . . . . . . . . . . . . 16
|
34 | 24, 1, 13, 25, 33, 2, 30, 6 | dib1dim2 36457 |
. . . . . . . . . . . . . . 15
|
35 | 32, 34 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
|
36 | | dih1dimat.s |
. . . . . . . . . . . . . . . . . 18
|
37 | 24, 1, 29, 2, 36 | dihf11 36556 |
. . . . . . . . . . . . . . . . 17
|
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
39 | | f1fn 6102 |
. . . . . . . . . . . . . . . 16
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
|
41 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . 15
|
42 | 40, 26, 41 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
43 | 35, 42 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
44 | 43 | adantrr 753 |
. . . . . . . . . . . 12
|
45 | 44 | adantr 481 |
. . . . . . . . . . 11
|
46 | 22, 45 | eqeltrd 2701 |
. . . . . . . . . 10
|
47 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
|
48 | | dih1dimat.d |
. . . . . . . . . . . . . . . . . . 19
Scalar |
49 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 1, 14, 2, 48, 49 | dvhbase 36372 |
. . . . . . . . . . . . . . . . . 18
|
51 | 47, 50 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | rexeqdv 3145 |
. . . . . . . . . . . . . . . 16
|
53 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 55 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | | dih1dimat.m |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | 1, 13, 14, 2, 57 | dvhvscacl 36392 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | 53, 54, 56, 58 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . 19
|
60 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . 17
|
63 | 62 | pm4.71rd 667 |
. . . . . . . . . . . . . . . 16
|
64 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . 21
|
67 | 66 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | 1, 13, 14, 2, 57 | dvhopvsca 36391 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 53, 54, 65, 67, 68 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
71 | 70 | rexbidva 3049 |
. . . . . . . . . . . . . . . . 17
|
72 | 71 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
|
73 | 52, 63, 72 | 3bitrd 294 |
. . . . . . . . . . . . . . 15
|
74 | 73 | abbidv 2741 |
. . . . . . . . . . . . . 14
|
75 | | df-rab 2921 |
. . . . . . . . . . . . . 14
|
76 | 74, 75 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
77 | | ssrab2 3687 |
. . . . . . . . . . . . . . 15
|
78 | | relxp 5227 |
. . . . . . . . . . . . . . 15
|
79 | | relss 5206 |
. . . . . . . . . . . . . . 15
|
80 | 77, 78, 79 | mp2 9 |
. . . . . . . . . . . . . 14
|
81 | | relopab 5247 |
. . . . . . . . . . . . . 14
|
82 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
83 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
84 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | anbi1d 741 |
. . . . . . . . . . . . . . . 16
|
86 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . 18
|
87 | 86 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
88 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
89 | 87, 88 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
90 | 82, 83, 85, 89 | opelopab 4997 |
. . . . . . . . . . . . . . 15
|
91 | | dih1dimat.c |
. . . . . . . . . . . . . . . . . . 19
|
92 | | dih1dimat.p |
. . . . . . . . . . . . . . . . . . 19
|
93 | | dih1dimat.j |
. . . . . . . . . . . . . . . . . . 19
|
94 | | dih1dimat.g |
. . . . . . . . . . . . . . . . . . 19
|
95 | 1, 2, 29, 8, 24, 27, 91, 92, 13, 25, 14, 33, 48, 93, 5, 57, 36, 6, 7, 94 | dih1dimatlem0 36617 |
. . . . . . . . . . . . . . . . . 18
|
96 | 95 | 3expa 1265 |
. . . . . . . . . . . . . . . . 17
|
97 | | opelxp 5146 |
. . . . . . . . . . . . . . . . . 18
|
98 | 82, 83 | opth 4945 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 98 | rexbii 3041 |
. . . . . . . . . . . . . . . . . 18
|
100 | 97, 99 | anbi12i 733 |
. . . . . . . . . . . . . . . . 17
|
101 | 96, 100 | syl6bbr 278 |
. . . . . . . . . . . . . . . 16
|
102 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
|
103 | 102 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
104 | 103 | elrab 3363 |
. . . . . . . . . . . . . . . 16
|
105 | 101, 104 | syl6bbr 278 |
. . . . . . . . . . . . . . 15
|
106 | 90, 105 | syl5rbb 273 |
. . . . . . . . . . . . . 14
|
107 | 80, 81, 106 | eqrelrdv 5216 |
. . . . . . . . . . . . 13
|
108 | 76, 107 | eqtrd 2656 |
. . . . . . . . . . . 12
|
109 | 1, 2, 47 | dvhlmod 36399 |
. . . . . . . . . . . . 13
|
110 | 1, 13, 14, 2, 5 | dvhelvbasei 36377 |
. . . . . . . . . . . . . 14
|
111 | 110 | adantr 481 |
. . . . . . . . . . . . 13
|
112 | 48, 49, 5, 57, 6 | lspsn 19002 |
. . . . . . . . . . . . 13
|
113 | 109, 111,
112 | syl2anc 693 |
. . . . . . . . . . . 12
|
114 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
115 | 24, 1, 13, 14, 33, 2, 48, 93 | tendoinvcl 36393 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | simpld 475 |
. . . . . . . . . . . . . . . . 17
|
117 | 47, 66, 114, 116 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
118 | 1, 13, 14 | tendocl 36055 |
. . . . . . . . . . . . . . . 16
|
119 | 47, 117, 64, 118 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
120 | 27, 91, 1, 92 | lhpocnel2 35305 |
. . . . . . . . . . . . . . . 16
|
121 | 47, 120 | syl 17 |
. . . . . . . . . . . . . . 15
|
122 | 27, 91, 1, 13 | ltrnel 35425 |
. . . . . . . . . . . . . . 15
|
123 | 47, 119, 121, 122 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
124 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
125 | 27, 91, 1, 124, 29 | dihvalcqat 36528 |
. . . . . . . . . . . . . 14
|
126 | 47, 123, 125 | syl2anc 693 |
. . . . . . . . . . . . 13
|
127 | 27, 91, 1, 92, 13, 14, 124, 94 | dicval2 36468 |
. . . . . . . . . . . . . 14
|
128 | 47, 123, 127 | syl2anc 693 |
. . . . . . . . . . . . 13
|
129 | 126, 128 | eqtrd 2656 |
. . . . . . . . . . . 12
|
130 | 108, 113,
129 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
131 | 24, 1, 29 | dihfn 36557 |
. . . . . . . . . . . . . 14
|
132 | 131 | adantr 481 |
. . . . . . . . . . . . 13
|
133 | 132 | adantr 481 |
. . . . . . . . . . . 12
|
134 | | simplll 798 |
. . . . . . . . . . . . . . . 16
|
135 | | hlop 34649 |
. . . . . . . . . . . . . . . 16
|
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . 15
|
137 | 24, 1 | lhpbase 35284 |
. . . . . . . . . . . . . . . 16
|
138 | 137 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
|
139 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
140 | 24, 139 | opoccl 34481 |
. . . . . . . . . . . . . . 15
|
141 | 136, 138,
140 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
142 | 92, 141 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
143 | 24, 1, 13 | ltrncl 35411 |
. . . . . . . . . . . . 13
|
144 | 47, 119, 142, 143 | syl3anc 1326 |
. . . . . . . . . . . 12
|
145 | | fnfvelrn 6356 |
. . . . . . . . . . . 12
|
146 | 133, 144,
145 | syl2anc 693 |
. . . . . . . . . . 11
|
147 | 130, 146 | eqeltrd 2701 |
. . . . . . . . . 10
|
148 | 46, 147 | pm2.61dane 2881 |
. . . . . . . . 9
|
149 | 148 | ralrimivva 2971 |
. . . . . . . 8
|
150 | | sneq 4187 |
. . . . . . . . . . 11
|
151 | 150 | fveq2d 6195 |
. . . . . . . . . 10
|
152 | 151 | eleq1d 2686 |
. . . . . . . . 9
|
153 | 152 | ralxp 5263 |
. . . . . . . 8
|
154 | 149, 153 | sylibr 224 |
. . . . . . 7
|
155 | 154 | r19.21bi 2932 |
. . . . . 6
|
156 | 18, 155 | syldan 487 |
. . . . 5
|
157 | | eleq1a 2696 |
. . . . 5
|
158 | 156, 157 | syl 17 |
. . . 4
|
159 | 158 | rexlimdva 3031 |
. . 3
|
160 | 159 | adantr 481 |
. 2
|
161 | 11, 160 | mpd 15 |
1
|