Proof of Theorem rcaninv
Step | Hyp | Ref
| Expression |
1 | | rcaninv.b |
. . . . . 6
|
2 | | eqid 2622 |
. . . . . 6
|
3 | | eqid 2622 |
. . . . . 6
comp comp |
4 | | rcaninv.c |
. . . . . 6
|
5 | | rcaninv.y |
. . . . . 6
|
6 | | rcaninv.x |
. . . . . 6
|
7 | | eqid 2622 |
. . . . . . . 8
|
8 | 1, 2, 7, 4, 5, 6 | isohom 16436 |
. . . . . . 7
|
9 | | rcaninv.f |
. . . . . . 7
|
10 | 8, 9 | sseldd 3604 |
. . . . . 6
|
11 | 1, 2, 7, 4, 6, 5 | isohom 16436 |
. . . . . . 7
|
12 | | rcaninv.n |
. . . . . . . . 9
Inv |
13 | 1, 12, 4, 5, 6, 7 | invf 16428 |
. . . . . . . 8
|
14 | 13, 9 | ffvelrnd 6360 |
. . . . . . 7
|
15 | 11, 14 | sseldd 3604 |
. . . . . 6
|
16 | | rcaninv.z |
. . . . . 6
|
17 | | rcaninv.g |
. . . . . 6
|
18 | 1, 2, 3, 4, 5, 6, 5, 10, 15, 16, 17 | catass 16347 |
. . . . 5
comp
comp comp comp |
19 | | eqid 2622 |
. . . . . . . 8
|
20 | | eqid 2622 |
. . . . . . . 8
comp comp |
21 | 1, 7, 12, 4, 5, 6,
9, 19, 20 | invcoisoid 16452 |
. . . . . . 7
comp |
22 | 21 | eqcomd 2628 |
. . . . . 6
comp |
23 | 22 | oveq2d 6666 |
. . . . 5
comp comp comp |
24 | 1, 2, 19, 4, 5, 3,
16, 17 | catrid 16345 |
. . . . 5
comp |
25 | 18, 23, 24 | 3eqtr2rd 2663 |
. . . 4
comp comp |
26 | 25 | adantr 481 |
. . 3
comp
comp |
27 | | rcaninv.o |
. . . . . . . . 9
comp |
28 | 27 | eqcomi 2631 |
. . . . . . . 8
comp |
29 | 28 | a1i 11 |
. . . . . . 7
comp |
30 | | eqidd 2623 |
. . . . . . 7
|
31 | | rcaninv.1 |
. . . . . . . . 9
|
32 | 31 | eqcomi 2631 |
. . . . . . . 8
|
33 | 32 | a1i 11 |
. . . . . . 7
|
34 | 29, 30, 33 | oveq123d 6671 |
. . . . . 6
comp |
35 | 34 | adantr 481 |
. . . . 5
comp |
36 | | simpr 477 |
. . . . 5
|
37 | 35, 36 | eqtrd 2656 |
. . . 4
comp |
38 | 37 | oveq1d 6665 |
. . 3
comp comp comp |
39 | 27 | oveqi 6663 |
. . . . . . 7
comp |
40 | 39 | oveq1i 6660 |
. . . . . 6
comp comp comp |
41 | 40 | a1i 11 |
. . . . 5
comp
comp
comp |
42 | 31, 15 | syl5eqel 2705 |
. . . . . . 7
|
43 | | rcaninv.h |
. . . . . . 7
|
44 | 1, 2, 3, 4, 5, 6, 5, 10, 42, 16, 43 | catass 16347 |
. . . . . 6
comp
comp comp comp |
45 | 31 | oveq1i 6660 |
. . . . . . . 8
comp comp |
46 | 45 | oveq2i 6661 |
. . . . . . 7
comp comp comp comp |
47 | 46 | a1i 11 |
. . . . . 6
comp
comp
comp
comp |
48 | 21 | oveq2d 6666 |
. . . . . 6
comp
comp
comp |
49 | 44, 47, 48 | 3eqtrd 2660 |
. . . . 5
comp
comp comp |
50 | 1, 2, 19, 4, 5, 3,
16, 43 | catrid 16345 |
. . . . 5
comp |
51 | 41, 49, 50 | 3eqtrd 2660 |
. . . 4
comp |
52 | 51 | adantr 481 |
. . 3
comp |
53 | 26, 38, 52 | 3eqtrd 2660 |
. 2
|
54 | 53 | ex 450 |
1
|