Step | Hyp | Ref
| Expression |
1 | | cycpm3.c |
. . . . 5
β’ πΆ = (toCycβπ·) |
2 | | cycpm3.s |
. . . . 5
β’ π = (SymGrpβπ·) |
3 | | cycpm3.d |
. . . . 5
β’ (π β π· β π) |
4 | | cycpm3.i |
. . . . 5
β’ (π β πΌ β π·) |
5 | | cycpm3.j |
. . . . 5
β’ (π β π½ β π·) |
6 | | cycpm3.k |
. . . . 5
β’ (π β πΎ β π·) |
7 | | cycpm3.1 |
. . . . 5
β’ (π β πΌ β π½) |
8 | | cycpm3.2 |
. . . . 5
β’ (π β π½ β πΎ) |
9 | | cycpm3.3 |
. . . . 5
β’ (π β πΎ β πΌ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cycpm3cl 32281 |
. . . 4
β’ (π β (πΆββ¨βπΌπ½πΎββ©) β (Baseβπ)) |
11 | | eqid 2732 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
12 | 2, 11 | symgbasf 19237 |
. . . 4
β’ ((πΆββ¨βπΌπ½πΎββ©) β (Baseβπ) β (πΆββ¨βπΌπ½πΎββ©):π·βΆπ·) |
13 | 10, 12 | syl 17 |
. . 3
β’ (π β (πΆββ¨βπΌπ½πΎββ©):π·βΆπ·) |
14 | 13 | ffnd 6715 |
. 2
β’ (π β (πΆββ¨βπΌπ½πΎββ©) Fn π·) |
15 | 2 | symggrp 19262 |
. . . . . 6
β’ (π· β π β π β Grp) |
16 | 3, 15 | syl 17 |
. . . . 5
β’ (π β π β Grp) |
17 | 9 | necomd 2996 |
. . . . . 6
β’ (π β πΌ β πΎ) |
18 | 1, 3, 4, 6, 17, 2 | cycpm2cl 32266 |
. . . . 5
β’ (π β (πΆββ¨βπΌπΎββ©) β (Baseβπ)) |
19 | 1, 3, 4, 5, 7, 2 | cycpm2cl 32266 |
. . . . 5
β’ (π β (πΆββ¨βπΌπ½ββ©) β (Baseβπ)) |
20 | | cyc3co2.t |
. . . . . 6
β’ Β· =
(+gβπ) |
21 | 11, 20 | grpcl 18823 |
. . . . 5
β’ ((π β Grp β§ (πΆββ¨βπΌπΎββ©) β (Baseβπ) β§ (πΆββ¨βπΌπ½ββ©) β (Baseβπ)) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) β (Baseβπ)) |
22 | 16, 18, 19, 21 | syl3anc 1371 |
. . . 4
β’ (π β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) β (Baseβπ)) |
23 | 2, 11 | symgbasf 19237 |
. . . 4
β’ (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) β (Baseβπ) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)):π·βΆπ·) |
24 | 22, 23 | syl 17 |
. . 3
β’ (π β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)):π·βΆπ·) |
25 | 24 | ffnd 6715 |
. 2
β’ (π β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) Fn π·) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc3fv1 32283 |
. . . . . . . 8
β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπΌ) = π½) |
27 | 26 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½πΎββ©)βπΌ) = π½) |
28 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π₯ = πΌ) β π₯ = πΌ) |
29 | 28 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = ((πΆββ¨βπΌπ½πΎββ©)βπΌ)) |
30 | 2, 11, 20 | symgov 19245 |
. . . . . . . . . . 11
β’ (((πΆββ¨βπΌπΎββ©) β (Baseβπ) β§ (πΆββ¨βπΌπ½ββ©) β (Baseβπ)) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) = ((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))) |
31 | 18, 19, 30 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) = ((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))) |
32 | 31 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) = ((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))) |
33 | 32 | fveq1d 6890 |
. . . . . . . 8
β’ ((π β§ π₯ = πΌ) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯)) |
34 | 2, 11 | symgbasf 19237 |
. . . . . . . . . . . 12
β’ ((πΆββ¨βπΌπ½ββ©) β (Baseβπ) β (πΆββ¨βπΌπ½ββ©):π·βΆπ·) |
35 | 19, 34 | syl 17 |
. . . . . . . . . . 11
β’ (π β (πΆββ¨βπΌπ½ββ©):π·βΆπ·) |
36 | 35 | ffund 6718 |
. . . . . . . . . 10
β’ (π β Fun (πΆββ¨βπΌπ½ββ©)) |
37 | 4 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΌ) β πΌ β π·) |
38 | 34 | fdmd 6725 |
. . . . . . . . . . . . 13
β’ ((πΆββ¨βπΌπ½ββ©) β (Baseβπ) β dom (πΆββ¨βπΌπ½ββ©) = π·) |
39 | 19, 38 | syl 17 |
. . . . . . . . . . . 12
β’ (π β dom (πΆββ¨βπΌπ½ββ©) = π·) |
40 | 39 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΌ) β dom (πΆββ¨βπΌπ½ββ©) = π·) |
41 | 37, 28, 40 | 3eltr4d 2848 |
. . . . . . . . . 10
β’ ((π β§ π₯ = πΌ) β π₯ β dom (πΆββ¨βπΌπ½ββ©)) |
42 | | fvco 6986 |
. . . . . . . . . 10
β’ ((Fun
(πΆββ¨βπΌπ½ββ©) β§ π₯ β dom (πΆββ¨βπΌπ½ββ©)) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯))) |
43 | 36, 41, 42 | syl2an2r 683 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΌ) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯))) |
44 | 28 | fveq2d 6892 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = ((πΆββ¨βπΌπ½ββ©)βπΌ)) |
45 | 1, 3, 4, 5, 7, 2 | cyc2fv1 32267 |
. . . . . . . . . . . 12
β’ (π β ((πΆββ¨βπΌπ½ββ©)βπΌ) = π½) |
46 | 45 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½ββ©)βπΌ) = π½) |
47 | 44, 46 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = π½) |
48 | 47 | fveq2d 6892 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯)) = ((πΆββ¨βπΌπΎββ©)βπ½)) |
49 | 8 | necomd 2996 |
. . . . . . . . . . 11
β’ (π β πΎ β π½) |
50 | 7 | necomd 2996 |
. . . . . . . . . . 11
β’ (π β π½ β πΌ) |
51 | 1, 2, 3, 4, 6, 5, 17, 49, 50 | cyc2fvx 32280 |
. . . . . . . . . 10
β’ (π β ((πΆββ¨βπΌπΎββ©)βπ½) = π½) |
52 | 51 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπΎββ©)βπ½) = π½) |
53 | 43, 48, 52 | 3eqtrd 2776 |
. . . . . . . 8
β’ ((π β§ π₯ = πΌ) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = π½) |
54 | 33, 53 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π₯ = πΌ) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = π½) |
55 | 27, 29, 54 | 3eqtr4d 2782 |
. . . . . 6
β’ ((π β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
56 | 55 | adantlr 713 |
. . . . 5
β’ (((π β§ π₯ β {πΌ, π½, πΎ}) β§ π₯ = πΌ) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
57 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc3fv2 32284 |
. . . . . . . 8
β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπ½) = πΎ) |
58 | 57 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπ½πΎββ©)βπ½) = πΎ) |
59 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π₯ = π½) β π₯ = π½) |
60 | 59 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = ((πΆββ¨βπΌπ½πΎββ©)βπ½)) |
61 | 31 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) = ((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))) |
62 | 61 | fveq1d 6890 |
. . . . . . . 8
β’ ((π β§ π₯ = π½) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯)) |
63 | 5 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = π½) β π½ β π·) |
64 | 39 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = π½) β dom (πΆββ¨βπΌπ½ββ©) = π·) |
65 | 63, 59, 64 | 3eltr4d 2848 |
. . . . . . . . . 10
β’ ((π β§ π₯ = π½) β π₯ β dom (πΆββ¨βπΌπ½ββ©)) |
66 | 36, 65, 42 | syl2an2r 683 |
. . . . . . . . 9
β’ ((π β§ π₯ = π½) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯))) |
67 | 59 | fveq2d 6892 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = ((πΆββ¨βπΌπ½ββ©)βπ½)) |
68 | 1, 3, 4, 5, 7, 2 | cyc2fv2 32268 |
. . . . . . . . . . . 12
β’ (π β ((πΆββ¨βπΌπ½ββ©)βπ½) = πΌ) |
69 | 68 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπ½ββ©)βπ½) = πΌ) |
70 | 67, 69 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = πΌ) |
71 | 70 | fveq2d 6892 |
. . . . . . . . 9
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯)) = ((πΆββ¨βπΌπΎββ©)βπΌ)) |
72 | 1, 3, 4, 6, 17, 2 | cyc2fv1 32267 |
. . . . . . . . . 10
β’ (π β ((πΆββ¨βπΌπΎββ©)βπΌ) = πΎ) |
73 | 72 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπΎββ©)βπΌ) = πΎ) |
74 | 66, 71, 73 | 3eqtrd 2776 |
. . . . . . . 8
β’ ((π β§ π₯ = π½) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = πΎ) |
75 | 62, 74 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π₯ = π½) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = πΎ) |
76 | 58, 60, 75 | 3eqtr4d 2782 |
. . . . . 6
β’ ((π β§ π₯ = π½) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
77 | 76 | adantlr 713 |
. . . . 5
β’ (((π β§ π₯ β {πΌ, π½, πΎ}) β§ π₯ = π½) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
78 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc3fv3 32285 |
. . . . . . . 8
β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπΎ) = πΌ) |
79 | 78 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½πΎββ©)βπΎ) = πΌ) |
80 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π₯ = πΎ) β π₯ = πΎ) |
81 | 80 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = ((πΆββ¨βπΌπ½πΎββ©)βπΎ)) |
82 | 31 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) = ((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))) |
83 | 82 | fveq1d 6890 |
. . . . . . . 8
β’ ((π β§ π₯ = πΎ) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯)) |
84 | 6 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΎ) β πΎ β π·) |
85 | 39 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΎ) β dom (πΆββ¨βπΌπ½ββ©) = π·) |
86 | 84, 80, 85 | 3eltr4d 2848 |
. . . . . . . . . 10
β’ ((π β§ π₯ = πΎ) β π₯ β dom (πΆββ¨βπΌπ½ββ©)) |
87 | 36, 86, 42 | syl2an2r 683 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΎ) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯))) |
88 | 80 | fveq2d 6892 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = ((πΆββ¨βπΌπ½ββ©)βπΎ)) |
89 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc2fvx 32280 |
. . . . . . . . . . . 12
β’ (π β ((πΆββ¨βπΌπ½ββ©)βπΎ) = πΎ) |
90 | 89 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½ββ©)βπΎ) = πΎ) |
91 | 88, 90 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = πΎ) |
92 | 91 | fveq2d 6892 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯)) = ((πΆββ¨βπΌπΎββ©)βπΎ)) |
93 | 1, 3, 4, 6, 17, 2 | cyc2fv2 32268 |
. . . . . . . . . 10
β’ (π β ((πΆββ¨βπΌπΎββ©)βπΎ) = πΌ) |
94 | 93 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπΎββ©)βπΎ) = πΌ) |
95 | 87, 92, 94 | 3eqtrd 2776 |
. . . . . . . 8
β’ ((π β§ π₯ = πΎ) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = πΌ) |
96 | 83, 95 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π₯ = πΎ) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = πΌ) |
97 | 79, 81, 96 | 3eqtr4d 2782 |
. . . . . 6
β’ ((π β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
98 | 97 | adantlr 713 |
. . . . 5
β’ (((π β§ π₯ β {πΌ, π½, πΎ}) β§ π₯ = πΎ) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
99 | | eltpi 4690 |
. . . . . 6
β’ (π₯ β {πΌ, π½, πΎ} β (π₯ = πΌ β¨ π₯ = π½ β¨ π₯ = πΎ)) |
100 | 99 | adantl 482 |
. . . . 5
β’ ((π β§ π₯ β {πΌ, π½, πΎ}) β (π₯ = πΌ β¨ π₯ = π½ β¨ π₯ = πΎ)) |
101 | 56, 77, 98, 100 | mpjao3dan 1431 |
. . . 4
β’ ((π β§ π₯ β {πΌ, π½, πΎ}) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
102 | 101 | adantlr 713 |
. . 3
β’ (((π β§ π₯ β π·) β§ π₯ β {πΌ, π½, πΎ}) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
103 | 35 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β (πΆββ¨βπΌπ½ββ©):π·βΆπ·) |
104 | 103 | ffund 6718 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β Fun (πΆββ¨βπΌπ½ββ©)) |
105 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β π₯ β (π· β {πΌ, π½, πΎ})) |
106 | 105 | eldifad 3959 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β π₯ β π·) |
107 | 39 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β dom (πΆββ¨βπΌπ½ββ©) = π·) |
108 | 106, 107 | eleqtrrd 2836 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β π₯ β dom (πΆββ¨βπΌπ½ββ©)) |
109 | 104, 108,
42 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯))) |
110 | 3 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β π· β π) |
111 | 4, 5 | s2cld 14818 |
. . . . . . . . 9
β’ (π β β¨βπΌπ½ββ© β Word π·) |
112 | 111 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β β¨βπΌπ½ββ© β Word π·) |
113 | 4, 5, 7 | s2f1 32098 |
. . . . . . . . 9
β’ (π β β¨βπΌπ½ββ©:dom β¨βπΌπ½ββ©β1-1βπ·) |
114 | 113 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β β¨βπΌπ½ββ©:dom β¨βπΌπ½ββ©β1-1βπ·) |
115 | | tpid1g 4772 |
. . . . . . . . . . . . 13
β’ (πΌ β π· β πΌ β {πΌ, π½, πΎ}) |
116 | 4, 115 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΌ β {πΌ, π½, πΎ}) |
117 | | tpid2g 4774 |
. . . . . . . . . . . . 13
β’ (π½ β π· β π½ β {πΌ, π½, πΎ}) |
118 | 5, 117 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π½ β {πΌ, π½, πΎ}) |
119 | 116, 118 | prssd 4824 |
. . . . . . . . . . 11
β’ (π β {πΌ, π½} β {πΌ, π½, πΎ}) |
120 | 4, 5 | s2rn 32097 |
. . . . . . . . . . . 12
β’ (π β ran β¨βπΌπ½ββ© = {πΌ, π½}) |
121 | 120 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (π β {πΌ, π½} = ran β¨βπΌπ½ββ©) |
122 | 4, 5, 6 | s3rn 32099 |
. . . . . . . . . . . 12
β’ (π β ran β¨βπΌπ½πΎββ© = {πΌ, π½, πΎ}) |
123 | 122 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (π β {πΌ, π½, πΎ} = ran β¨βπΌπ½πΎββ©) |
124 | 119, 121,
123 | 3sstr3d 4027 |
. . . . . . . . . 10
β’ (π β ran β¨βπΌπ½ββ© β ran β¨βπΌπ½πΎββ©) |
125 | 124 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ran β¨βπΌπ½ββ© β ran β¨βπΌπ½πΎββ©) |
126 | 105 | eldifbd 3960 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β Β¬ π₯ β {πΌ, π½, πΎ}) |
127 | 122 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ran β¨βπΌπ½πΎββ© = {πΌ, π½, πΎ}) |
128 | 126, 127 | neleqtrrd 2856 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β Β¬ π₯ β ran β¨βπΌπ½πΎββ©) |
129 | 125, 128 | ssneldd 3984 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β Β¬ π₯ β ran β¨βπΌπ½ββ©) |
130 | 1, 110, 112, 114, 106, 129 | cycpmfv3 32261 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπ½ββ©)βπ₯) = π₯) |
131 | 130 | fveq2d 6892 |
. . . . . 6
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπΎββ©)β((πΆββ¨βπΌπ½ββ©)βπ₯)) = ((πΆββ¨βπΌπΎββ©)βπ₯)) |
132 | 4, 6 | s2cld 14818 |
. . . . . . . 8
β’ (π β β¨βπΌπΎββ© β Word π·) |
133 | 132 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β β¨βπΌπΎββ© β Word π·) |
134 | 4, 6, 17 | s2f1 32098 |
. . . . . . . 8
β’ (π β β¨βπΌπΎββ©:dom β¨βπΌπΎββ©β1-1βπ·) |
135 | 134 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β β¨βπΌπΎββ©:dom β¨βπΌπΎββ©β1-1βπ·) |
136 | | tpid3g 4775 |
. . . . . . . . . . . 12
β’ (πΎ β π· β πΎ β {πΌ, π½, πΎ}) |
137 | 6, 136 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΎ β {πΌ, π½, πΎ}) |
138 | 116, 137 | prssd 4824 |
. . . . . . . . . 10
β’ (π β {πΌ, πΎ} β {πΌ, π½, πΎ}) |
139 | 138 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β {πΌ, πΎ} β {πΌ, π½, πΎ}) |
140 | 4, 6 | s2rn 32097 |
. . . . . . . . . . 11
β’ (π β ran β¨βπΌπΎββ© = {πΌ, πΎ}) |
141 | 140 | eqcomd 2738 |
. . . . . . . . . 10
β’ (π β {πΌ, πΎ} = ran β¨βπΌπΎββ©) |
142 | 141 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β {πΌ, πΎ} = ran β¨βπΌπΎββ©) |
143 | 123 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β {πΌ, π½, πΎ} = ran β¨βπΌπ½πΎββ©) |
144 | 139, 142,
143 | 3sstr3d 4027 |
. . . . . . . 8
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ran β¨βπΌπΎββ© β ran β¨βπΌπ½πΎββ©) |
145 | 144, 128 | ssneldd 3984 |
. . . . . . 7
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β Β¬ π₯ β ran β¨βπΌπΎββ©) |
146 | 1, 110, 133, 135, 106, 145 | cycpmfv3 32261 |
. . . . . 6
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπΎββ©)βπ₯) = π₯) |
147 | 109, 131,
146 | 3eqtrd 2776 |
. . . . 5
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯) = π₯) |
148 | 31 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©)) = ((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))) |
149 | 148 | fveq1d 6890 |
. . . . 5
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯) = (((πΆββ¨βπΌπΎββ©) β (πΆββ¨βπΌπ½ββ©))βπ₯)) |
150 | 4, 5, 6 | s3cld 14819 |
. . . . . . 7
β’ (π β β¨βπΌπ½πΎββ© β Word π·) |
151 | 150 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β β¨βπΌπ½πΎββ© β Word π·) |
152 | 4, 5, 6, 7, 8, 9 | s3f1 32100 |
. . . . . . 7
β’ (π β β¨βπΌπ½πΎββ©:dom β¨βπΌπ½πΎββ©β1-1βπ·) |
153 | 152 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β β¨βπΌπ½πΎββ©:dom β¨βπΌπ½πΎββ©β1-1βπ·) |
154 | 1, 110, 151, 153, 106, 128 | cycpmfv3 32261 |
. . . . 5
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = π₯) |
155 | 147, 149,
154 | 3eqtr4rd 2783 |
. . . 4
β’ ((π β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
156 | 155 | adantlr 713 |
. . 3
β’ (((π β§ π₯ β π·) β§ π₯ β (π· β {πΌ, π½, πΎ})) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
157 | | tpssi 4838 |
. . . . . . . 8
β’ ((πΌ β π· β§ π½ β π· β§ πΎ β π·) β {πΌ, π½, πΎ} β π·) |
158 | 4, 5, 6, 157 | syl3anc 1371 |
. . . . . . 7
β’ (π β {πΌ, π½, πΎ} β π·) |
159 | | undif 4480 |
. . . . . . 7
β’ ({πΌ, π½, πΎ} β π· β ({πΌ, π½, πΎ} βͺ (π· β {πΌ, π½, πΎ})) = π·) |
160 | 158, 159 | sylib 217 |
. . . . . 6
β’ (π β ({πΌ, π½, πΎ} βͺ (π· β {πΌ, π½, πΎ})) = π·) |
161 | 160 | eleq2d 2819 |
. . . . 5
β’ (π β (π₯ β ({πΌ, π½, πΎ} βͺ (π· β {πΌ, π½, πΎ})) β π₯ β π·)) |
162 | 161 | biimpar 478 |
. . . 4
β’ ((π β§ π₯ β π·) β π₯ β ({πΌ, π½, πΎ} βͺ (π· β {πΌ, π½, πΎ}))) |
163 | | elun 4147 |
. . . 4
β’ (π₯ β ({πΌ, π½, πΎ} βͺ (π· β {πΌ, π½, πΎ})) β (π₯ β {πΌ, π½, πΎ} β¨ π₯ β (π· β {πΌ, π½, πΎ}))) |
164 | 162, 163 | sylib 217 |
. . 3
β’ ((π β§ π₯ β π·) β (π₯ β {πΌ, π½, πΎ} β¨ π₯ β (π· β {πΌ, π½, πΎ}))) |
165 | 102, 156,
164 | mpjaodan 957 |
. 2
β’ ((π β§ π₯ β π·) β ((πΆββ¨βπΌπ½πΎββ©)βπ₯) = (((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))βπ₯)) |
166 | 14, 25, 165 | eqfnfvd 7032 |
1
β’ (π β (πΆββ¨βπΌπ½πΎββ©) = ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))) |