Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dih1dimatlem Unicode version

Theorem dih1dimatlem 32141
 Description: Lemma for dih1dimat 32142. (Contributed by NM, 10-Apr-2014.)
Hypotheses
Ref Expression
dih1dimat.h
dih1dimat.u
dih1dimat.i
dih1dimat.a LSAtoms
dih1dimat.b
dih1dimat.l
dih1dimat.c
dih1dimat.p
dih1dimat.t
dih1dimat.r
dih1dimat.e
dih1dimat.o
dih1dimat.d Scalar
dih1dimat.j
dih1dimat.v
dih1dimat.m
dih1dimat.s
dih1dimat.n
dih1dimat.z
dih1dimat.g
Assertion
Ref Expression
dih1dimatlem
Distinct variable groups:   ,   ,   ,,   ,   ,   ,,   ,,,   ,,,   ,,,   ,,,   ,,   ,,,   ,,   ,
Allowed substitution hints:   (,,)   (,)   (,)   (,,)   (,)   (,,)   (,,)   (,,)   ()   (,,)   (,,)   ()   (,)   (,)   ()   (,,)   ()   (,,)

Proof of Theorem dih1dimatlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dih1dimat.h . . . . 5
2 dih1dimat.u . . . . 5
3 id 19 . . . . 5
41, 2, 3dvhlvec 31921 . . . 4
5 dih1dimat.v . . . . 5
6 dih1dimat.n . . . . 5
7 dih1dimat.z . . . . 5
8 dih1dimat.a . . . . 5 LSAtoms
95, 6, 7, 8islsat 29803 . . . 4
104, 9syl 15 . . 3
1110biimpa 470 . 2
12 eldifi 3311 . . . . . . . 8
13 dih1dimat.t . . . . . . . . . 10
14 dih1dimat.e . . . . . . . . . 10
151, 13, 14, 2, 5dvhvbase 31899 . . . . . . . . 9
1615eleq2d 2363 . . . . . . . 8
1712, 16syl5ib 210 . . . . . . 7
1817imp 418 . . . . . 6
19 simpr 447 . . . . . . . . . . . . . 14
2019opeq2d 3819 . . . . . . . . . . . . 13
2120sneqd 3666 . . . . . . . . . . . 12
2221fveq2d 5545 . . . . . . . . . . 11
23 simpl 443 . . . . . . . . . . . . . . . 16
24 dih1dimat.b . . . . . . . . . . . . . . . . 17
25 dih1dimat.r . . . . . . . . . . . . . . . . 17
2624, 1, 13, 25trlcl 30975 . . . . . . . . . . . . . . . 16
27 dih1dimat.l . . . . . . . . . . . . . . . . 17
2827, 1, 13, 25trlle 30995 . . . . . . . . . . . . . . . 16
29 dih1dimat.i . . . . . . . . . . . . . . . . 17
30 eqid 2296 . . . . . . . . . . . . . . . . 17
3124, 27, 1, 29, 30dihvalb 32049 . . . . . . . . . . . . . . . 16
3223, 26, 28, 31syl12anc 1180 . . . . . . . . . . . . . . 15
33 dih1dimat.o . . . . . . . . . . . . . . . 16
3424, 1, 13, 25, 33, 2, 30, 6dib1dim2 31980 . . . . . . . . . . . . . . 15
3532, 34eqtr2d 2329 . . . . . . . . . . . . . 14
36 dih1dimat.s . . . . . . . . . . . . . . . . . 18
3724, 1, 29, 2, 36dihf11 32079 . . . . . . . . . . . . . . . . 17
3837adantr 451 . . . . . . . . . . . . . . . 16
39 f1fn 5454 . . . . . . . . . . . . . . . 16
4038, 39syl 15 . . . . . . . . . . . . . . 15
41 fnfvelrn 5678 . . . . . . . . . . . . . . 15
4240, 26, 41syl2anc 642 . . . . . . . . . . . . . 14
4335, 42eqeltrd 2370 . . . . . . . . . . . . 13
4443adantrr 697 . . . . . . . . . . . 12
4544adantr 451 . . . . . . . . . . 11
4622, 45eqeltrd 2370 . . . . . . . . . 10
47 simpll 730 . . . . . . . . . . . . . . . . . 18
48 dih1dimat.d . . . . . . . . . . . . . . . . . . 19 Scalar
49 eqid 2296 . . . . . . . . . . . . . . . . . . 19
501, 14, 2, 48, 49dvhbase 31895 . . . . . . . . . . . . . . . . . 18
5147, 50syl 15 . . . . . . . . . . . . . . . . 17
5251rexeqdv 2756 . . . . . . . . . . . . . . . 16
53 simplll 734 . . . . . . . . . . . . . . . . . . . 20
54 simpr 447 . . . . . . . . . . . . . . . . . . . 20
55 simpllr 735 . . . . . . . . . . . . . . . . . . . . 21
56 opelxpi 4737 . . . . . . . . . . . . . . . . . . . . 21
5755, 56syl 15 . . . . . . . . . . . . . . . . . . . 20
58 dih1dimat.m . . . . . . . . . . . . . . . . . . . . 21
591, 13, 14, 2, 58dvhvscacl 31915 . . . . . . . . . . . . . . . . . . . 20
6053, 54, 57, 59syl12anc 1180 . . . . . . . . . . . . . . . . . . 19
61 eleq1a 2365 . . . . . . . . . . . . . . . . . . 19
6260, 61syl 15 . . . . . . . . . . . . . . . . . 18
6362rexlimdva 2680 . . . . . . . . . . . . . . . . 17
6463pm4.71rd 616 . . . . . . . . . . . . . . . 16
65 simplrl 736 . . . . . . . . . . . . . . . . . . . . 21
6665adantr 451 . . . . . . . . . . . . . . . . . . . 20
67 simplrr 737 . . . . . . . . . . . . . . . . . . . . 21
6867adantr 451 . . . . . . . . . . . . . . . . . . . 20
691, 13, 14, 2, 58dvhopvsca 31914 . . . . . . . . . . . . . . . . . . . 20
7053, 54, 66, 68, 69syl13anc 1184 . . . . . . . . . . . . . . . . . . 19
7170eqeq2d 2307 . . . . . . . . . . . . . . . . . 18
7271rexbidva 2573 . . . . . . . . . . . . . . . . 17
7372anbi2d 684 . . . . . . . . . . . . . . . 16
7452, 64, 733bitrd 270 . . . . . . . . . . . . . . 15
7574abbidv 2410 . . . . . . . . . . . . . 14
76 df-rab 2565 . . . . . . . . . . . . . 14
7775, 76syl6eqr 2346 . . . . . . . . . . . . 13
78 ssrab2 3271 . . . . . . . . . . . . . . 15
79 relxp 4810 . . . . . . . . . . . . . . 15
80 relss 4791 . . . . . . . . . . . . . . 15
8178, 79, 80mp2 17 . . . . . . . . . . . . . 14
82 relopab 4828 . . . . . . . . . . . . . 14
83 vex 2804 . . . . . . . . . . . . . . . 16
84 vex 2804 . . . . . . . . . . . . . . . 16
85 eqeq1 2302 . . . . . . . . . . . . . . . . 17
8685anbi1d 685 . . . . . . . . . . . . . . . 16
87 fveq1 5540 . . . . . . . . . . . . . . . . . 18
8887eqeq2d 2307 . . . . . . . . . . . . . . . . 17
89 eleq1 2356 . . . . . . . . . . . . . . . . 17
9088, 89anbi12d 691 . . . . . . . . . . . . . . . 16
9183, 84, 86, 90opelopab 4302 . . . . . . . . . . . . . . 15
92 dih1dimat.c . . . . . . . . . . . . . . . . . . 19
93 dih1dimat.p . . . . . . . . . . . . . . . . . . 19
94 dih1dimat.j . . . . . . . . . . . . . . . . . . 19
95 dih1dimat.g . . . . . . . . . . . . . . . . . . 19
961, 2, 29, 8, 24, 27, 92, 93, 13, 25, 14, 33, 48, 94, 5, 58, 36, 6, 7, 95dih1dimatlem0 32140 . . . . . . . . . . . . . . . . . 18
97963expa 1151 . . . . . . . . . . . . . . . . 17
98 opelxp 4735 . . . . . . . . . . . . . . . . . 18
9983, 84opth 4261 . . . . . . . . . . . . . . . . . . 19
10099rexbii 2581 . . . . . . . . . . . . . . . . . 18
10198, 100anbi12i 678 . . . . . . . . . . . . . . . . 17
10297, 101syl6bbr 254 . . . . . . . . . . . . . . . 16
103 eqeq1 2302 . . . . . . . . . . . . . . . . . 18
104103rexbidv 2577 . . . . . . . . . . . . . . . . 17
105104elrab 2936 . . . . . . . . . . . . . . . 16
106102, 105syl6bbr 254 . . . . . . . . . . . . . . 15
10791, 106syl5rbb 249 . . . . . . . . . . . . . 14
10881, 82, 107eqrelrdv 4799 . . . . . . . . . . . . 13
10977, 108eqtrd 2328 . . . . . . . . . . . 12
1101, 2, 47dvhlmod 31922 . . . . . . . . . . . . 13
1111, 13, 14, 2, 5dvhelvbasei 31900 . . . . . . . . . . . . . 14
112111adantr 451 . . . . . . . . . . . . 13
11348, 49, 5, 58, 6lspsn 15775 . . . . . . . . . . . . 13
114110, 112, 113syl2anc 642 . . . . . . . . . . . 12
115 simpr 447 . . . . . . . . . . . . . . . . 17
11624, 1, 13, 14, 33, 2, 48, 94tendoinvcl 31916 . . . . . . . . . . . . . . . . . 18
117116simpld 445 . . . . . . . . . . . . . . . . 17
11847, 67, 115, 117syl3anc 1182 . . . . . . . . . . . . . . . 16
1191, 13, 14tendocl 31578 . . . . . . . . . . . . . . . 16
12047, 118, 65, 119syl3anc 1182 . . . . . . . . . . . . . . 15
12127, 92, 1, 93lhpocnel2 30830 . . . . . . . . . . . . . . . 16
12247, 121syl 15 . . . . . . . . . . . . . . 15
12327, 92, 1, 13ltrnel 30950 . . . . . . . . . . . . . . 15
12447, 120, 122, 123syl3anc 1182 . . . . . . . . . . . . . 14
125 eqid 2296 . . . . . . . . . . . . . . 15
12627, 92, 1, 125, 29dihvalcqat 32051 . . . . . . . . . . . . . 14
12747, 124, 126syl2anc 642 . . . . . . . . . . . . 13
12827, 92, 1, 93, 13, 14, 125, 95dicval2 31991 . . . . . . . . . . . . . 14
12947, 124, 128syl2anc 642 . . . . . . . . . . . . 13
130127, 129eqtrd 2328 . . . . . . . . . . . 12
131109, 114, 1303eqtr4d 2338 . . . . . . . . . . 11
13224, 1, 29dihfn 32080 . . . . . . . . . . . . . 14
133132adantr 451 . . . . . . . . . . . . 13
134133adantr 451 . . . . . . . . . . . 12
135 simplll 734 . . . . . . . . . . . . . . . 16
136 hlop 30174 . . . . . . . . . . . . . . . 16
137135, 136syl 15 . . . . . . . . . . . . . . 15
138 simpllr 735 . . . . . . . . . . . . . . . 16
13924, 1lhpbase 30809 . . . . . . . . . . . . . . . 16
140138, 139syl 15 . . . . . . . . . . . . . . 15
141 eqid 2296 . . . . . . . . . . . . . . . 16
14224, 141opoccl 30006 . . . . . . . . . . . . . . 15
143137, 140, 142syl2anc 642 . . . . . . . . . . . . . 14
14493, 143syl5eqel 2380 . . . . . . . . . . . . 13
14524, 1, 13ltrncl 30936 . . . . . . . . . . . . 13
14647, 120, 144, 145syl3anc 1182 . . . . . . . . . . . 12
147 fnfvelrn 5678 . . . . . . . . . . . 12
148134, 146, 147syl2anc 642 . . . . . . . . . . 11
149131, 148eqeltrd 2370 . . . . . . . . . 10
15046, 149pm2.61dane 2537 . . . . . . . . 9
151150ralrimivva 2648 . . . . . . . 8
152 sneq 3664 . . . . . . . . . . 11
153152fveq2d 5545 . . . . . . . . . 10
154153eleq1d 2362 . . . . . . . . 9
155154ralxp 4843 . . . . . . . 8
156151, 155sylibr 203 . . . . . . 7
157156r19.21bi 2654 . . . . . 6
15818, 157syldan 456 . . . . 5
159 eleq1a 2365 . . . . 5
160158, 159syl 15 . . . 4
161160rexlimdva 2680 . . 3