Step | Hyp | Ref
| Expression |
1 | | frgpnabl.a |
. . . . . . 7
β’ (π β π΄ β πΌ) |
2 | | 0ex 5269 |
. . . . . . . . 9
β’ β
β V |
3 | 2 | prid1 4728 |
. . . . . . . 8
β’ β
β {β
, 1o} |
4 | | df2o3 8425 |
. . . . . . . 8
β’
2o = {β
, 1o} |
5 | 3, 4 | eleqtrri 2837 |
. . . . . . 7
β’ β
β 2o |
6 | | opelxpi 5675 |
. . . . . . 7
β’ ((π΄ β πΌ β§ β
β 2o) β
β¨π΄, β
β©
β (πΌ Γ
2o)) |
7 | 1, 5, 6 | sylancl 587 |
. . . . . 6
β’ (π β β¨π΄, β
β© β (πΌ Γ 2o)) |
8 | | frgpnabl.b |
. . . . . . 7
β’ (π β π΅ β πΌ) |
9 | | opelxpi 5675 |
. . . . . . 7
β’ ((π΅ β πΌ β§ β
β 2o) β
β¨π΅, β
β©
β (πΌ Γ
2o)) |
10 | 8, 5, 9 | sylancl 587 |
. . . . . 6
β’ (π β β¨π΅, β
β© β (πΌ Γ 2o)) |
11 | 7, 10 | s2cld 14767 |
. . . . 5
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β Word (πΌ Γ
2o)) |
12 | | frgpnabl.w |
. . . . . 6
β’ π = ( I βWord (πΌ Γ
2o)) |
13 | | frgpnabl.i |
. . . . . . . 8
β’ (π β πΌ β π) |
14 | | 2on 8431 |
. . . . . . . 8
β’
2o β On |
15 | | xpexg 7689 |
. . . . . . . 8
β’ ((πΌ β π β§ 2o β On) β
(πΌ Γ 2o)
β V) |
16 | 13, 14, 15 | sylancl 587 |
. . . . . . 7
β’ (π β (πΌ Γ 2o) β
V) |
17 | | wrdexg 14419 |
. . . . . . 7
β’ ((πΌ Γ 2o) β V
β Word (πΌ Γ
2o) β V) |
18 | | fvi 6922 |
. . . . . . 7
β’ (Word
(πΌ Γ 2o)
β V β ( I βWord (πΌ Γ 2o)) = Word (πΌ Γ
2o)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . 6
β’ (π β ( I βWord (πΌ Γ 2o)) = Word
(πΌ Γ
2o)) |
20 | 12, 19 | eqtrid 2789 |
. . . . 5
β’ (π β π = Word (πΌ Γ 2o)) |
21 | 11, 20 | eleqtrrd 2841 |
. . . 4
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β π) |
22 | | 1n0 8439 |
. . . . . . 7
β’
1o β β
|
23 | | 2cn 12235 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
24 | 23 | addid2i 11350 |
. . . . . . . . . . . . 13
β’ (0 + 2) =
2 |
25 | | s2len 14785 |
. . . . . . . . . . . . 13
β’
(β―ββ¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©) =
2 |
26 | 24, 25 | eqtr4i 2768 |
. . . . . . . . . . . 12
β’ (0 + 2) =
(β―ββ¨ββ¨π΄, β
β©β¨π΅,
β
β©ββ©) |
27 | | frgpnabl.r |
. . . . . . . . . . . . . 14
β’ βΌ = (
~FG βπΌ) |
28 | | frgpnabl.m |
. . . . . . . . . . . . . 14
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
29 | | frgpnabl.t |
. . . . . . . . . . . . . 14
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
30 | 12, 27, 28, 29 | efgtlen 19515 |
. . . . . . . . . . . . 13
β’ ((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) β
(β―ββ¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©) =
((β―βπ₯) +
2)) |
31 | 30 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) β
(β―ββ¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©) =
((β―βπ₯) +
2)) |
32 | 26, 31 | eqtrid 2789 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) β (0 + 2) = ((β―βπ₯) + 2)) |
33 | 32 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯) β (0 + 2) =
((β―βπ₯) +
2))) |
34 | | 0cnd 11155 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β 0 β β) |
35 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β π₯ β π) |
36 | 12 | efgrcl 19504 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
37 | 36 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π β π = Word (πΌ Γ 2o)) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β π = Word (πΌ Γ 2o)) |
39 | 35, 38 | eleqtrd 2840 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β π₯ β Word (πΌ Γ 2o)) |
40 | | lencl 14428 |
. . . . . . . . . . . . 13
β’ (π₯ β Word (πΌ Γ 2o) β
(β―βπ₯) β
β0) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β (β―βπ₯) β
β0) |
42 | 41 | nn0cnd 12482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (β―βπ₯) β β) |
43 | | 2cnd 12238 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β 2 β β) |
44 | 34, 42, 43 | addcan2d 11366 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β ((0 + 2) = ((β―βπ₯) + 2) β 0 =
(β―βπ₯))) |
45 | 33, 44 | sylibd 238 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯) β 0 =
(β―βπ₯))) |
46 | 12, 27, 28, 29 | efgtf 19511 |
. . . . . . . . . . . . . . . . . 18
β’ (β
β π β ((πββ
) = (π β
(0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πββ
):((0...(β―ββ
))
Γ (πΌ Γ
2o))βΆπ)) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ β
β π) β ((πββ
) = (π β (0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πββ
):((0...(β―ββ
))
Γ (πΌ Γ
2o))βΆπ)) |
48 | 47 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ β
β π) β (πββ
) = (π β (0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
49 | 48 | rneqd 5898 |
. . . . . . . . . . . . . . 15
β’ ((π β§ β
β π) β ran (πββ
) = ran (π β (0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©))) |
50 | 49 | eleq2d 2824 |
. . . . . . . . . . . . . 14
β’ ((π β§ β
β π) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β ran (πββ
) β
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β ran (π β (0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)))) |
51 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π β
(0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) = (π β (0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
52 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
β’ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©) β
V |
53 | 51, 52 | elrnmpo 7497 |
. . . . . . . . . . . . . . 15
β’
(β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(π β
(0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β βπ β
(0...(β―ββ
))βπ β (πΌ Γ
2o)β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© = (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
54 | | wrd0 14434 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β Word (πΌ Γ
2o) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β β
β Word (πΌ Γ
2o)) |
56 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π β (πΌ Γ 2o)) |
57 | 28 | efgmf 19502 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π:(πΌ Γ 2o)βΆ(πΌ Γ
2o) |
58 | 57 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πΌ Γ 2o) β (πβπ) β (πΌ Γ 2o)) |
59 | 56, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β (πβπ) β (πΌ Γ 2o)) |
60 | 56, 59 | s2cld 14767 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β
β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o)) |
61 | | ccatidid 14485 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β
++ β
) = β
|
62 | 61 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β
++ β
) ++ β
) = (β
++ β
) |
63 | 62, 61 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
=
((β
++ β
) ++ β
) |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β β
=
((β
++ β
) ++ β
)) |
65 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π β
(0...(β―ββ
))) |
66 | | hash0 14274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(β―ββ
) = 0 |
67 | 66 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(0...(β―ββ
)) = (0...0) |
68 | 65, 67 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π β
(0...0)) |
69 | | elfz1eq 13459 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...0) β π = 0) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π = 0) |
71 | 70, 66 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π =
(β―ββ
)) |
72 | 66 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π + (β―ββ
)) =
(π + 0) |
73 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
β |
74 | 70, 73 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π β
β) |
75 | 74 | addid1d 11362 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β (π + 0) = π) |
76 | 72, 75 | eqtr2id 2790 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β π = (π + (β―ββ
))) |
77 | 55, 55, 55, 60, 64, 71, 76 | splval2 14652 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©) = ((β
++
β¨βπ(πβπ)ββ©) ++ β
)) |
78 | | ccatlid 14481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β (β
++
β¨βπ(πβπ)ββ©) = β¨βπ(πβπ)ββ©) |
79 | 78 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β ((β
++
β¨βπ(πβπ)ββ©) ++ β
) =
(β¨βπ(πβπ)ββ© ++ β
)) |
80 | | ccatrid 14482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β
(β¨βπ(πβπ)ββ© ++ β
) =
β¨βπ(πβπ)ββ©) |
81 | 79, 80 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β ((β
++
β¨βπ(πβπ)ββ©) ++ β
) =
β¨βπ(πβπ)ββ©) |
82 | 60, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β ((β
++ β¨βπ(πβπ)ββ©) ++ β
) =
β¨βπ(πβπ)ββ©) |
83 | 77, 82 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©) = β¨βπ(πβπ)ββ©) |
84 | 83 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©) β
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©)) |
85 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β π΄ β πΌ) |
86 | | 1on 8429 |
. . . . . . . . . . . . . . . . . . . 20
β’
1o β On |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β 1o β
On) |
88 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) |
89 | 88 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ©β1) = (β¨βπ(πβπ)ββ©β1)) |
90 | | opex 5426 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β¨π΅,
β
β© β V |
91 | | s2fv1 14784 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨π΅,
β
β© β V β (β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©β1) =
β¨π΅,
β
β©) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©β1) =
β¨π΅,
β
β© |
93 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πβπ) β V |
94 | | s2fv1 14784 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβπ) β V β (β¨βπ(πβπ)ββ©β1) = (πβπ)) |
95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨βπ(πβπ)ββ©β1) = (πβπ) |
96 | 89, 92, 95 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β β¨π΅, β
β© = (πβπ)) |
97 | 88 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ©β0) = (β¨βπ(πβπ)ββ©β0)) |
98 | | opex 5426 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β¨π΄,
β
β© β V |
99 | | s2fv0 14783 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(β¨π΄,
β
β© β V β (β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©β0) =
β¨π΄,
β
β©) |
100 | 98, 99 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©β0) =
β¨π΄,
β
β© |
101 | | s2fv0 14783 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β V β
(β¨βπ(πβπ)ββ©β0) = π) |
102 | 101 | elv 3454 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨βπ(πβπ)ββ©β0) = π |
103 | 97, 100, 102 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β β¨π΄, β
β© = π) |
104 | 103 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β (πββ¨π΄, β
β©) = (πβπ)) |
105 | 28 | efgmval 19501 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β πΌ β§ β
β 2o) β
(π΄πβ
) = β¨π΄, (1o β
β
)β©) |
106 | 85, 5, 105 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β (π΄πβ
) = β¨π΄, (1o β
β
)β©) |
107 | | df-ov 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄πβ
) = (πββ¨π΄, β
β©) |
108 | | dif0 4337 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(1o β β
) = 1o |
109 | 108 | opeq2i 4839 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β¨π΄,
(1o β β
)β© = β¨π΄, 1oβ© |
110 | 106, 107,
109 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β (πββ¨π΄, β
β©) = β¨π΄, 1oβ©) |
111 | 96, 104, 110 | 3eqtr2rd 2784 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β β¨π΄, 1oβ© =
β¨π΅,
β
β©) |
112 | | opthg 5439 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β πΌ β§ 1o β On) β
(β¨π΄,
1oβ© = β¨π΅, β
β© β (π΄ = π΅ β§ 1o =
β
))) |
113 | 112 | simplbda 501 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β πΌ β§ 1o β On) β§
β¨π΄,
1oβ© = β¨π΅, β
β©) β 1o =
β
) |
114 | 85, 87, 111, 113 | syl21anc 837 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β§
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ©) β 1o =
β
) |
115 | 114 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = β¨βπ(πβπ)ββ© β 1o =
β
)) |
116 | 84, 115 | sylbid 239 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ β
β π) β§ (π β (0...(β―ββ
)) β§
π β (πΌ Γ 2o))) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© = (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©) β 1o =
β
)) |
117 | 116 | rexlimdvva 3206 |
. . . . . . . . . . . . . . 15
β’ ((π β§ β
β π) β (βπ β
(0...(β―ββ
))βπ β (πΌ Γ
2o)β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© = (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©) β 1o =
β
)) |
118 | 53, 117 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’ ((π β§ β
β π) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β ran (π β (0...(β―ββ
)), π β (πΌ Γ 2o) β¦ (β
splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β 1o =
β
)) |
119 | 50, 118 | sylbid 239 |
. . . . . . . . . . . . 13
β’ ((π β§ β
β π) β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β ran (πββ
) β 1o =
β
)) |
120 | 119 | expimpd 455 |
. . . . . . . . . . . 12
β’ (π β ((β
β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πββ
)) β 1o =
β
)) |
121 | | hasheq0 14270 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β V β
((β―βπ₯) = 0
β π₯ =
β
)) |
122 | 121 | elv 3454 |
. . . . . . . . . . . . . . 15
β’
((β―βπ₯) =
0 β π₯ =
β
) |
123 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = β
β (π₯ β π β β
β π)) |
124 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = β
β (πβπ₯) = (πββ
)) |
125 | 124 | rneqd 5898 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β
β ran (πβπ₯) = ran (πββ
)) |
126 | 125 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = β
β
(β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β ran (πβπ₯) β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πββ
))) |
127 | 123, 126 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π₯ = β
β ((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) β (β
β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πββ
)))) |
128 | 122, 127 | sylbi 216 |
. . . . . . . . . . . . . 14
β’
((β―βπ₯) =
0 β ((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯)) β (β
β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πββ
)))) |
129 | 128 | eqcoms 2745 |
. . . . . . . . . . . . 13
β’ (0 =
(β―βπ₯) β
((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯)) β (β
β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πββ
)))) |
130 | 129 | imbi1d 342 |
. . . . . . . . . . . 12
β’ (0 =
(β―βπ₯) β
(((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯)) β 1o =
β
) β ((β
β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πββ
)) β
1o = β
))) |
131 | 120, 130 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ (π β (0 = (β―βπ₯) β ((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) β 1o =
β
))) |
132 | 131 | com23 86 |
. . . . . . . . . 10
β’ (π β ((π₯ β π β§ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) β (0 = (β―βπ₯) β 1o =
β
))) |
133 | 132 | expdimp 454 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯) β (0 =
(β―βπ₯) β
1o = β
))) |
134 | 45, 133 | mpdd 43 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯) β 1o =
β
)) |
135 | 134 | necon3ad 2957 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (1o β β
β
Β¬ β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β ran (πβπ₯))) |
136 | 22, 135 | mpi 20 |
. . . . . 6
β’ ((π β§ π₯ β π) β Β¬ β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ran (πβπ₯)) |
137 | 136 | nrexdv 3147 |
. . . . 5
β’ (π β Β¬ βπ₯ β π β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) |
138 | | eliun 4963 |
. . . . 5
β’
(β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β βͺ π₯ β π ran (πβπ₯) β βπ₯ β π β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β ran
(πβπ₯)) |
139 | 137, 138 | sylnibr 329 |
. . . 4
β’ (π β Β¬
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ© β βͺ π₯ β π ran (πβπ₯)) |
140 | 21, 139 | eldifd 3926 |
. . 3
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β (π β βͺ π₯ β π ran (πβπ₯))) |
141 | | frgpnabl.d |
. . 3
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
142 | 140, 141 | eleqtrrdi 2849 |
. 2
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β π·) |
143 | | df-s2 14744 |
. . . . 5
β’
β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© =
(β¨ββ¨π΄,
β
β©ββ© ++ β¨ββ¨π΅,
β
β©ββ©) |
144 | 12, 27 | efger 19507 |
. . . . . . 7
β’ βΌ Er
π |
145 | 144 | a1i 11 |
. . . . . 6
β’ (π β βΌ Er π) |
146 | 145, 21 | erref 8675 |
. . . . 5
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
βΌ
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ©) |
147 | 143, 146 | eqbrtrrid 5146 |
. . . 4
β’ (π β (β¨ββ¨π΄, β
β©ββ© ++
β¨ββ¨π΅,
β
β©ββ©) βΌ
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ©) |
148 | 143 | ovexi 7396 |
. . . . 5
β’
β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β
V |
149 | | ovex 7395 |
. . . . 5
β’
(β¨ββ¨π΄, β
β©ββ© ++
β¨ββ¨π΅,
β
β©ββ©) β V |
150 | 148, 149 | elec 8699 |
. . . 4
β’
(β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ© β
[(β¨ββ¨π΄,
β
β©ββ© ++ β¨ββ¨π΅, β
β©ββ©)] βΌ β
(β¨ββ¨π΄,
β
β©ββ© ++ β¨ββ¨π΅, β
β©ββ©) βΌ
β¨ββ¨π΄,
β
β©β¨π΅,
β
β©ββ©) |
151 | 147, 150 | sylibr 233 |
. . 3
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β [(β¨ββ¨π΄, β
β©ββ© ++
β¨ββ¨π΅,
β
β©ββ©)] βΌ ) |
152 | | frgpnabl.u |
. . . . . . 7
β’ π =
(varFGrpβπΌ) |
153 | 27, 152 | vrgpval 19556 |
. . . . . 6
β’ ((πΌ β π β§ π΄ β πΌ) β (πβπ΄) = [β¨ββ¨π΄, β
β©ββ©] βΌ
) |
154 | 13, 1, 153 | syl2anc 585 |
. . . . 5
β’ (π β (πβπ΄) = [β¨ββ¨π΄, β
β©ββ©] βΌ
) |
155 | 27, 152 | vrgpval 19556 |
. . . . . 6
β’ ((πΌ β π β§ π΅ β πΌ) β (πβπ΅) = [β¨ββ¨π΅, β
β©ββ©] βΌ
) |
156 | 13, 8, 155 | syl2anc 585 |
. . . . 5
β’ (π β (πβπ΅) = [β¨ββ¨π΅, β
β©ββ©] βΌ
) |
157 | 154, 156 | oveq12d 7380 |
. . . 4
β’ (π β ((πβπ΄) + (πβπ΅)) = ([β¨ββ¨π΄, β
β©ββ©] βΌ +
[β¨ββ¨π΅,
β
β©ββ©] βΌ )) |
158 | 7 | s1cld 14498 |
. . . . . 6
β’ (π β β¨ββ¨π΄, β
β©ββ©
β Word (πΌ Γ
2o)) |
159 | 158, 20 | eleqtrrd 2841 |
. . . . 5
β’ (π β β¨ββ¨π΄, β
β©ββ©
β π) |
160 | 10 | s1cld 14498 |
. . . . . 6
β’ (π β β¨ββ¨π΅, β
β©ββ©
β Word (πΌ Γ
2o)) |
161 | 160, 20 | eleqtrrd 2841 |
. . . . 5
β’ (π β β¨ββ¨π΅, β
β©ββ©
β π) |
162 | | frgpnabl.g |
. . . . . 6
β’ πΊ = (freeGrpβπΌ) |
163 | | frgpnabl.p |
. . . . . 6
β’ + =
(+gβπΊ) |
164 | 12, 162, 27, 163 | frgpadd 19552 |
. . . . 5
β’
((β¨ββ¨π΄, β
β©ββ© β π β§ β¨ββ¨π΅, β
β©ββ©
β π) β
([β¨ββ¨π΄,
β
β©ββ©] βΌ + [β¨ββ¨π΅, β
β©ββ©]
βΌ
) = [(β¨ββ¨π΄,
β
β©ββ© ++ β¨ββ¨π΅, β
β©ββ©)] βΌ
) |
165 | 159, 161,
164 | syl2anc 585 |
. . . 4
β’ (π β ([β¨ββ¨π΄, β
β©ββ©]
βΌ
+
[β¨ββ¨π΅,
β
β©ββ©] βΌ ) =
[(β¨ββ¨π΄,
β
β©ββ© ++ β¨ββ¨π΅, β
β©ββ©)] βΌ
) |
166 | 157, 165 | eqtrd 2777 |
. . 3
β’ (π β ((πβπ΄) + (πβπ΅)) = [(β¨ββ¨π΄, β
β©ββ© ++
β¨ββ¨π΅,
β
β©ββ©)] βΌ ) |
167 | 151, 166 | eleqtrrd 2841 |
. 2
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β ((πβπ΄) + (πβπ΅))) |
168 | 142, 167 | elind 4159 |
1
β’ (π β β¨ββ¨π΄, β
β©β¨π΅, β
β©ββ©
β (π· β© ((πβπ΄) + (πβπ΅)))) |