Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem27 Structured version   Visualization version   Unicode version

Theorem poimirlem27 32031
 Description: Lemma for poimir 32037 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0
poimirlem28.1
poimirlem28.2
poimirlem28.3
poimirlem28.4
Assertion
Ref Expression
poimirlem27 ..^ ..^
Distinct variable groups:   ,,,,,,   ,,   ,,   ,,,,   ,,,,,,   ,,,,,,,   ,,,,,   ,,,,
Allowed substitution hints:   ()   ()   (,,)

Proof of Theorem poimirlem27
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfi 12223 . . . . . 6
2 fzfi 12223 . . . . . 6
3 mapfi 7888 . . . . . 6
41, 2, 3mp2an 686 . . . . 5
5 fzfi 12223 . . . . 5
6 mapfi 7888 . . . . 5
74, 5, 6mp2an 686 . . . 4
87a1i 11 . . 3
9 2z 10993 . . . 4
109a1i 11 . . 3
11 fzofi 12225 . . . . . . . 8 ..^
12 mapfi 7888 . . . . . . . 8 ..^ ..^
1311, 2, 12mp2an 686 . . . . . . 7 ..^
14 mapfi 7888 . . . . . . . . 9
152, 2, 14mp2an 686 . . . . . . . 8
16 f1of 5828 . . . . . . . . . 10
1716ss2abi 3487 . . . . . . . . 9
18 ovex 6336 . . . . . . . . . 10
1918, 18mapval 7502 . . . . . . . . 9
2017, 19sseqtr4i 3451 . . . . . . . 8
21 ssfi 7810 . . . . . . . 8
2215, 20, 21mp2an 686 . . . . . . 7
23 xpfi 7860 . . . . . . 7 ..^ ..^
2413, 22, 23mp2an 686 . . . . . 6 ..^
25 fzfi 12223 . . . . . 6
26 xpfi 7860 . . . . . 6 ..^ ..^
2724, 25, 26mp2an 686 . . . . 5 ..^
28 rabfi 7814 . . . . 5 ..^ ..^
2927, 28ax-mp 5 . . . 4 ..^
30 hashcl 12576 . . . . 5 ..^ ..^
3130nn0zd 11061 . . . 4 ..^ ..^
3229, 31mp1i 13 . . 3 ..^
33 dfrex2 2837 . . . . 5 ..^ ..^
34 nfv 1769 . . . . . 6
35 nfcv 2612 . . . . . . 7
36 nfcv 2612 . . . . . . 7
37 nfcv 2612 . . . . . . . 8
38 nfrab1 2957 . . . . . . . 8 ..^
3937, 38nffv 5886 . . . . . . 7 ..^
4035, 36, 39nfbr 4440 . . . . . 6 ..^
41 neq0 3733 . . . . . . . . . . . 12 ..^ ..^
42 iddvds 14393 . . . . . . . . . . . . . . . . 17
439, 42ax-mp 5 . . . . . . . . . . . . . . . 16
44 vex 3034 . . . . . . . . . . . . . . . . . . 19
45 hashsng 12587 . . . . . . . . . . . . . . . . . . 19
4644, 45ax-mp 5 . . . . . . . . . . . . . . . . . 18
4746oveq2i 6319 . . . . . . . . . . . . . . . . 17
48 df-2 10690 . . . . . . . . . . . . . . . . 17
4947, 48eqtr4i 2496 . . . . . . . . . . . . . . . 16
5043, 49breqtrri 4421 . . . . . . . . . . . . . . 15
51 rabfi 7814 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
52 diffi 7821 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
5327, 51, 52mp2b 10 . . . . . . . . . . . . . . . . . . 19 ..^
54 snfi 7668 . . . . . . . . . . . . . . . . . . 19
55 incom 3616 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
56 disjdif 3830 . . . . . . . . . . . . . . . . . . . 20 ..^
5755, 56eqtri 2493 . . . . . . . . . . . . . . . . . . 19 ..^
58 hashun 12599 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
5953, 54, 57, 58mp3an 1390 . . . . . . . . . . . . . . . . . 18 ..^ ..^
60 difsnid 4109 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^
6160fveq2d 5883 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
6259, 61syl5eqr 2519 . . . . . . . . . . . . . . . . 17 ..^ ..^ ..^
6362adantl 473 . . . . . . . . . . . . . . . 16 ..^ ..^ ..^
64 poimir.0 . . . . . . . . . . . . . . . . . . . 20
6564ad3antrrr 744 . . . . . . . . . . . . . . . . . . 19 ..^
66 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6766breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6867ifbid 3894 . . . . . . . . . . . . . . . . . . . . . . . . 25
6968csbeq1d 3356 . . . . . . . . . . . . . . . . . . . . . . . 24
70 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7170fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7270fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7372imaeq1d 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7473xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7572imaeq1d 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7675xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7774, 76uneq12d 3580 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7871, 77oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . 25
7978csbeq2dv 3785 . . . . . . . . . . . . . . . . . . . . . . . 24
8069, 79eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . 23
8180mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . 22
82 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26
84 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8582, 83, 84ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . . . . 25
8685csbeq1d 3356 . . . . . . . . . . . . . . . . . . . . . . . 24
87 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8887imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8988xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
90 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9190oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9291imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9392xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9489, 93uneq12d 3580 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9594oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . 25
9695cbvcsbv 3355 . . . . . . . . . . . . . . . . . . . . . . . 24
9786, 96syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . 23
9897cbvmptv 4488 . . . . . . . . . . . . . . . . . . . . . 22
9981, 98syl6eq 2521 . . . . . . . . . . . . . . . . . . . . 21
10099eqeq2d 2481 . . . . . . . . . . . . . . . . . . . 20
101100cbvrabv 3030 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
102 elmapi 7511 . . . . . . . . . . . . . . . . . . . 20
103102ad3antlr 745 . . . . . . . . . . . . . . . . . . 19 ..^
104 simpr 468 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
105 simpl 464 . . . . . . . . . . . . . . . . . . . . . 22
106105ralimi 2796 . . . . . . . . . . . . . . . . . . . . 21
107106ad2antlr 741 . . . . . . . . . . . . . . . . . . . 20 ..^
108 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
109108neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . . 23
110109rexbidv 2892 . . . . . . . . . . . . . . . . . . . . . 22
111 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . . . 24
112111neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . . 23
113112cbvrexv 3006 . . . . . . . . . . . . . . . . . . . . . 22
114110, 113syl6bb 269 . . . . . . . . . . . . . . . . . . . . 21
115114rspccva 3135 . . . . . . . . . . . . . . . . . . . 20
116107, 115sylan 479 . . . . . . . . . . . . . . . . . . 19 ..^
117 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22
118117ralimi 2796 . . . . . . . . . . . . . . . . . . . . 21
119118ad2antlr 741 . . . . . . . . . . . . . . . . . . . 20 ..^
120108neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . . 23
121120rexbidv 2892 . . . . . . . . . . . . . . . . . . . . . 22
122111neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . . 23
123122cbvrexv 3006 . . . . . . . . . . . . . . . . . . . . . 22
124121, 123syl6bb 269 . . . . . . . . . . . . . . . . . . . . 21
125124rspccva 3135 . . . . . . . . . . . . . . . . . . . 20
126119, 125sylan 479 . . . . . . . . . . . . . . . . . . 19 ..^
12765, 101, 103, 104, 116, 126poimirlem22 32026 . . . . . . . . . . . . . . . . . 18 ..^ ..^
128 eldifsn 4088 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
129128eubii 2341 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
13053elexi 3041 . . . . . . . . . . . . . . . . . . . 20 ..^
131 euhash1 12635 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^
132130, 131ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
133 df-reu 2763 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
134129, 132, 1333bitr4ri 286 . . . . . . . . . . . . . . . . . 18 ..^ ..^
135127, 134sylib 201 . . . . . . . . . . . . . . . . 17 ..^