Step | Hyp | Ref
| Expression |
1 | | pi1co.j |
. . 3
β’ (π β π½ β (TopOnβπ)) |
2 | | pi1co.a |
. . 3
β’ (π β π΄ β π) |
3 | | pi1co.p |
. . . 4
β’ π = (π½ Ο1 π΄) |
4 | 3 | pi1grp 24566 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β Grp) |
5 | 1, 2, 4 | syl2anc 585 |
. 2
β’ (π β π β Grp) |
6 | | pi1co.f |
. . . . 5
β’ (π β πΉ β (π½ Cn πΎ)) |
7 | | cntop2 22745 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β πΎ β Top) |
9 | | toptopon2 22420 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
10 | 8, 9 | sylib 217 |
. . 3
β’ (π β πΎ β (TopOnββͺ πΎ)) |
11 | | pi1co.b |
. . . 4
β’ (π β (πΉβπ΄) = π΅) |
12 | | cnf2 22753 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆβͺ πΎ) |
13 | 1, 10, 6, 12 | syl3anc 1372 |
. . . . 5
β’ (π β πΉ:πβΆβͺ πΎ) |
14 | 13, 2 | ffvelcdmd 7088 |
. . . 4
β’ (π β (πΉβπ΄) β βͺ πΎ) |
15 | 11, 14 | eqeltrrd 2835 |
. . 3
β’ (π β π΅ β βͺ πΎ) |
16 | | pi1co.q |
. . . 4
β’ π = (πΎ Ο1 π΅) |
17 | 16 | pi1grp 24566 |
. . 3
β’ ((πΎ β (TopOnββͺ πΎ)
β§ π΅ β βͺ πΎ)
β π β
Grp) |
18 | 10, 15, 17 | syl2anc 585 |
. 2
β’ (π β π β Grp) |
19 | | pi1co.v |
. . . 4
β’ π = (Baseβπ) |
20 | | pi1co.g |
. . . 4
β’ πΊ = ran (π β βͺ π β¦ β¨[π](
βphβπ½), [(πΉ β π)]( βphβπΎ)β©) |
21 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1cof 24575 |
. . 3
β’ (π β πΊ:πβΆ(Baseβπ)) |
22 | 19 | a1i 11 |
. . . . . . . 8
β’ (π β π = (Baseβπ)) |
23 | 3, 1, 2, 22 | pi1bas2 24557 |
. . . . . . 7
β’ (π β π = (βͺ π / (
βphβπ½))) |
24 | 23 | eleq2d 2820 |
. . . . . 6
β’ (π β (π¦ β π β π¦ β (βͺ π / (
βphβπ½)))) |
25 | 24 | biimpa 478 |
. . . . 5
β’ ((π β§ π¦ β π) β π¦ β (βͺ π / (
βphβπ½))) |
26 | | eqid 2733 |
. . . . . 6
β’ (βͺ π
/ ( βphβπ½)) = (βͺ π / (
βphβπ½)) |
27 | | fvoveq1 7432 |
. . . . . . . 8
β’ ([π](
βphβπ½) = π¦ β (πΊβ([π]( βphβπ½)(+gβπ)π§)) = (πΊβ(π¦(+gβπ)π§))) |
28 | | fveq2 6892 |
. . . . . . . . 9
β’ ([π](
βphβπ½) = π¦ β (πΊβ[π]( βphβπ½)) = (πΊβπ¦)) |
29 | 28 | oveq1d 7424 |
. . . . . . . 8
β’ ([π](
βphβπ½) = π¦ β ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§))) |
30 | 27, 29 | eqeq12d 2749 |
. . . . . . 7
β’ ([π](
βphβπ½) = π¦ β ((πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§)) β (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§)))) |
31 | 30 | ralbidv 3178 |
. . . . . 6
β’ ([π](
βphβπ½) = π¦ β (βπ§ β π (πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§)) β βπ§ β π (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§)))) |
32 | | oveq2 7417 |
. . . . . . . . . . 11
β’ ([β](
βphβπ½) = π§ β ([π]( βphβπ½)(+gβπ)[β]( βphβπ½)) = ([π]( βphβπ½)(+gβπ)π§)) |
33 | 32 | fveq2d 6896 |
. . . . . . . . . 10
β’ ([β](
βphβπ½) = π§ β (πΊβ([π]( βphβπ½)(+gβπ)[β]( βphβπ½))) = (πΊβ([π]( βphβπ½)(+gβπ)π§))) |
34 | | fveq2 6892 |
. . . . . . . . . . 11
β’ ([β](
βphβπ½) = π§ β (πΊβ[β]( βphβπ½)) = (πΊβπ§)) |
35 | 34 | oveq2d 7425 |
. . . . . . . . . 10
β’ ([β](
βphβπ½) = π§ β ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβ[β]( βphβπ½))) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§))) |
36 | 33, 35 | eqeq12d 2749 |
. . . . . . . . 9
β’ ([β](
βphβπ½) = π§ β ((πΊβ([π]( βphβπ½)(+gβπ)[β]( βphβπ½))) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβ[β]( βphβπ½))) β (πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§)))) |
37 | 3, 1, 2, 22 | pi1eluni 24558 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β βͺ π β (π β (II Cn π½) β§ (πβ0) = π΄ β§ (πβ1) = π΄))) |
38 | 37 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (π β (II Cn π½) β§ (πβ0) = π΄ β§ (πβ1) = π΄)) |
39 | 38 | simp1d 1143 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π) β π β (II Cn π½)) |
40 | 39 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β π β (II Cn π½)) |
41 | 1 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β βͺ π) β π½ β (TopOnβπ)) |
42 | 2 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β βͺ π) β π΄ β π) |
43 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β βͺ π) β π = (Baseβπ)) |
44 | 3, 41, 42, 43 | pi1eluni 24558 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (β β βͺ π β (β β (II Cn π½) β§ (ββ0) = π΄ β§ (ββ1) = π΄))) |
45 | 44 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (β β (II Cn π½) β§ (ββ0) = π΄ β§ (ββ1) = π΄)) |
46 | 45 | simp1d 1143 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β β β (II Cn π½)) |
47 | 38 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (πβ1) = π΄) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πβ1) = π΄) |
49 | 45 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (ββ0) = π΄) |
50 | 48, 49 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πβ1) = (ββ0)) |
51 | 6 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β πΉ β (π½ Cn πΎ)) |
52 | 40, 46, 50, 51 | copco 24534 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉ β (π(*πβπ½)β)) = ((πΉ β π)(*πβπΎ)(πΉ β β))) |
53 | 52 | eceq1d 8742 |
. . . . . . . . . . 11
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β [(πΉ β (π(*πβπ½)β))]( βphβπΎ) = [((πΉ β π)(*πβπΎ)(πΉ β β))]( βphβπΎ)) |
54 | 40, 46, 50 | pcocn 24533 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (π(*πβπ½)β) β (II Cn π½)) |
55 | 40, 46 | pco0 24530 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((π(*πβπ½)β)β0) = (πβ0)) |
56 | 38 | simp2d 1144 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (πβ0) = π΄) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πβ0) = π΄) |
58 | 55, 57 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((π(*πβπ½)β)β0) = π΄) |
59 | 40, 46 | pco1 24531 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((π(*πβπ½)β)β1) = (ββ1)) |
60 | 45 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (ββ1) = π΄) |
61 | 59, 60 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((π(*πβπ½)β)β1) = π΄) |
62 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β π½ β (TopOnβπ)) |
63 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β π΄ β π) |
64 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β π = (Baseβπ)) |
65 | 3, 62, 63, 64 | pi1eluni 24558 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((π(*πβπ½)β) β βͺ π β ((π(*πβπ½)β) β (II Cn π½) β§ ((π(*πβπ½)β)β0) = π΄ β§ ((π(*πβπ½)β)β1) = π΄))) |
66 | 54, 58, 61, 65 | mpbir3and 1343 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (π(*πβπ½)β) β βͺ π) |
67 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1coval 24576 |
. . . . . . . . . . . . 13
β’ ((π β§ (π(*πβπ½)β) β βͺ π) β (πΊβ[(π(*πβπ½)β)]( βphβπ½)) = [(πΉ β (π(*πβπ½)β))]( βphβπΎ)) |
68 | 67 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ (π(*πβπ½)β) β βͺ π) β (πΊβ[(π(*πβπ½)β)]( βphβπ½)) = [(πΉ β (π(*πβπ½)β))]( βphβπΎ)) |
69 | 66, 68 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΊβ[(π(*πβπ½)β)]( βphβπ½)) = [(πΉ β (π(*πβπ½)β))]( βphβπΎ)) |
70 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
71 | 10 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β πΎ β (TopOnββͺ πΎ)) |
72 | 15 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β π΅ β βͺ πΎ) |
73 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
74 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β πΉ β (π½ Cn πΎ)) |
75 | | cnco 22770 |
. . . . . . . . . . . . . . 15
β’ ((π β (II Cn π½) β§ πΉ β (π½ Cn πΎ)) β (πΉ β π) β (II Cn πΎ)) |
76 | 39, 74, 75 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π) β (πΉ β π) β (II Cn πΎ)) |
77 | | iitopon 24395 |
. . . . . . . . . . . . . . . . 17
β’ II β
(TopOnβ(0[,]1)) |
78 | | cnf2 22753 |
. . . . . . . . . . . . . . . . 17
β’ ((II
β (TopOnβ(0[,]1)) β§ π½ β (TopOnβπ) β§ π β (II Cn π½)) β π:(0[,]1)βΆπ) |
79 | 77, 41, 39, 78 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β βͺ π) β π:(0[,]1)βΆπ) |
80 | | 0elunit 13446 |
. . . . . . . . . . . . . . . 16
β’ 0 β
(0[,]1) |
81 | | fvco3 6991 |
. . . . . . . . . . . . . . . 16
β’ ((π:(0[,]1)βΆπ β§ 0 β (0[,]1)) β
((πΉ β π)β0) = (πΉβ(πβ0))) |
82 | 79, 80, 81 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β ((πΉ β π)β0) = (πΉβ(πβ0))) |
83 | 56 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (πΉβ(πβ0)) = (πΉβπ΄)) |
84 | 11 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (πΉβπ΄) = π΅) |
85 | 82, 83, 84 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π) β ((πΉ β π)β0) = π΅) |
86 | | 1elunit 13447 |
. . . . . . . . . . . . . . . 16
β’ 1 β
(0[,]1) |
87 | | fvco3 6991 |
. . . . . . . . . . . . . . . 16
β’ ((π:(0[,]1)βΆπ β§ 1 β (0[,]1)) β
((πΉ β π)β1) = (πΉβ(πβ1))) |
88 | 79, 86, 87 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β ((πΉ β π)β1) = (πΉβ(πβ1))) |
89 | 47 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (πΉβ(πβ1)) = (πΉβπ΄)) |
90 | 88, 89, 84 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π) β ((πΉ β π)β1) = π΅) |
91 | 10 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β πΎ β (TopOnββͺ πΎ)) |
92 | 15 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β π΅ β βͺ πΎ) |
93 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ π) β (Baseβπ) = (Baseβπ)) |
94 | 16, 91, 92, 93 | pi1eluni 24558 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ π) β ((πΉ β π) β βͺ
(Baseβπ) β
((πΉ β π) β (II Cn πΎ) β§ ((πΉ β π)β0) = π΅ β§ ((πΉ β π)β1) = π΅))) |
95 | 76, 85, 90, 94 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ π) β (πΉ β π) β βͺ
(Baseβπ)) |
96 | 95 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉ β π) β βͺ
(Baseβπ)) |
97 | | cnco 22770 |
. . . . . . . . . . . . . 14
β’ ((β β (II Cn π½) β§ πΉ β (π½ Cn πΎ)) β (πΉ β β) β (II Cn πΎ)) |
98 | 46, 51, 97 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉ β β) β (II Cn πΎ)) |
99 | | cnf2 22753 |
. . . . . . . . . . . . . . . 16
β’ ((II
β (TopOnβ(0[,]1)) β§ π½ β (TopOnβπ) β§ β β (II Cn π½)) β β:(0[,]1)βΆπ) |
100 | 77, 62, 46, 99 | mp3an2i 1467 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β β:(0[,]1)βΆπ) |
101 | | fvco3 6991 |
. . . . . . . . . . . . . . 15
β’ ((β:(0[,]1)βΆπ β§ 0 β (0[,]1)) β ((πΉ β β)β0) = (πΉβ(ββ0))) |
102 | 100, 80, 101 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((πΉ β β)β0) = (πΉβ(ββ0))) |
103 | 49 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉβ(ββ0)) = (πΉβπ΄)) |
104 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉβπ΄) = π΅) |
105 | 102, 103,
104 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((πΉ β β)β0) = π΅) |
106 | | fvco3 6991 |
. . . . . . . . . . . . . . 15
β’ ((β:(0[,]1)βΆπ β§ 1 β (0[,]1)) β ((πΉ β β)β1) = (πΉβ(ββ1))) |
107 | 100, 86, 106 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((πΉ β β)β1) = (πΉβ(ββ1))) |
108 | 60 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉβ(ββ1)) = (πΉβπ΄)) |
109 | 107, 108,
104 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((πΉ β β)β1) = π΅) |
110 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ (π β (Baseβπ) = (Baseβπ)) |
111 | 16, 10, 15, 110 | pi1eluni 24558 |
. . . . . . . . . . . . . 14
β’ (π β ((πΉ β β) β βͺ
(Baseβπ) β
((πΉ β β) β (II Cn πΎ) β§ ((πΉ β β)β0) = π΅ β§ ((πΉ β β)β1) = π΅))) |
112 | 111 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((πΉ β β) β βͺ
(Baseβπ) β
((πΉ β β) β (II Cn πΎ) β§ ((πΉ β β)β0) = π΅ β§ ((πΉ β β)β1) = π΅))) |
113 | 98, 105, 109, 112 | mpbir3and 1343 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΉ β β) β βͺ
(Baseβπ)) |
114 | 16, 70, 71, 72, 73, 96, 113 | pi1addval 24564 |
. . . . . . . . . . 11
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ([(πΉ β π)]( βphβπΎ)(+gβπ)[(πΉ β β)]( βphβπΎ)) = [((πΉ β π)(*πβπΎ)(πΉ β β))]( βphβπΎ)) |
115 | 53, 69, 114 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΊβ[(π(*πβπ½)β)]( βphβπ½)) = ([(πΉ β π)]( βphβπΎ)(+gβπ)[(πΉ β β)]( βphβπΎ))) |
116 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
117 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β π β βͺ π) |
118 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β β β βͺ π) |
119 | 3, 19, 62, 63, 116, 117, 118 | pi1addval 24564 |
. . . . . . . . . . 11
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ([π]( βphβπ½)(+gβπ)[β]( βphβπ½)) = [(π(*πβπ½)β)]( βphβπ½)) |
120 | 119 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΊβ([π]( βphβπ½)(+gβπ)[β]( βphβπ½))) = (πΊβ[(π(*πβπ½)β)]( βphβπ½))) |
121 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1coval 24576 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ π) β (πΊβ[π]( βphβπ½)) = [(πΉ β π)]( βphβπΎ)) |
122 | 121 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΊβ[π]( βphβπ½)) = [(πΉ β π)]( βphβπΎ)) |
123 | 3, 16, 19, 20, 1, 6, 2, 11 | pi1coval 24576 |
. . . . . . . . . . . 12
β’ ((π β§ β β βͺ π) β (πΊβ[β]( βphβπ½)) = [(πΉ β β)]( βphβπΎ)) |
124 | 123 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΊβ[β]( βphβπ½)) = [(πΉ β β)]( βphβπΎ)) |
125 | 122, 124 | oveq12d 7427 |
. . . . . . . . . 10
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβ[β]( βphβπ½))) = ([(πΉ β π)]( βphβπΎ)(+gβπ)[(πΉ β β)]( βphβπΎ))) |
126 | 115, 120,
125 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π β§ π β βͺ π) β§ β β βͺ π) β (πΊβ([π]( βphβπ½)(+gβπ)[β]( βphβπ½))) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβ[β]( βphβπ½)))) |
127 | 26, 36, 126 | ectocld 8778 |
. . . . . . . 8
β’ (((π β§ π β βͺ π) β§ π§ β (βͺ π / (
βphβπ½))) β (πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§))) |
128 | 127 | ralrimiva 3147 |
. . . . . . 7
β’ ((π β§ π β βͺ π) β βπ§ β (βͺ π
/ ( βphβπ½))(πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§))) |
129 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β βͺ π) β π = (βͺ π / (
βphβπ½))) |
130 | 129 | raleqdv 3326 |
. . . . . . 7
β’ ((π β§ π β βͺ π) β (βπ§ β π (πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§)) β βπ§ β (βͺ π / (
βphβπ½))(πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§)))) |
131 | 128, 130 | mpbird 257 |
. . . . . 6
β’ ((π β§ π β βͺ π) β βπ§ β π (πΊβ([π]( βphβπ½)(+gβπ)π§)) = ((πΊβ[π]( βphβπ½))(+gβπ)(πΊβπ§))) |
132 | 26, 31, 131 | ectocld 8778 |
. . . . 5
β’ ((π β§ π¦ β (βͺ π / (
βphβπ½))) β βπ§ β π (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§))) |
133 | 25, 132 | syldan 592 |
. . . 4
β’ ((π β§ π¦ β π) β βπ§ β π (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§))) |
134 | 133 | ralrimiva 3147 |
. . 3
β’ (π β βπ¦ β π βπ§ β π (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§))) |
135 | 21, 134 | jca 513 |
. 2
β’ (π β (πΊ:πβΆ(Baseβπ) β§ βπ¦ β π βπ§ β π (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§)))) |
136 | 19, 70, 116, 73 | isghm 19092 |
. 2
β’ (πΊ β (π GrpHom π) β ((π β Grp β§ π β Grp) β§ (πΊ:πβΆ(Baseβπ) β§ βπ¦ β π βπ§ β π (πΊβ(π¦(+gβπ)π§)) = ((πΊβπ¦)(+gβπ)(πΊβπ§))))) |
137 | 5, 18, 135, 136 | syl21anbrc 1345 |
1
β’ (π β πΊ β (π GrpHom π)) |