Step | Hyp | Ref
| Expression |
1 | | baseslid 12519 |
. 2
β’ (Base =
Slot (Baseβndx) β§ (Baseβndx) β β) |
2 | | 2str.g |
. . 3
β’ πΊ = {β¨(Baseβndx),
π΅β©, β¨(πΈβndx), + β©} |
3 | | basendxnn 12518 |
. . . . . 6
β’
(Baseβndx) β β |
4 | 3 | a1i 9 |
. . . . 5
β’ ((π΅ β π β§ + β π) β (Baseβndx) β
β) |
5 | | simpl 109 |
. . . . 5
β’ ((π΅ β π β§ + β π) β π΅ β π) |
6 | | opexg 4229 |
. . . . 5
β’
(((Baseβndx) β β β§ π΅ β π) β β¨(Baseβndx), π΅β© β
V) |
7 | 4, 5, 6 | syl2anc 411 |
. . . 4
β’ ((π΅ β π β§ + β π) β β¨(Baseβndx), π΅β© β
V) |
8 | | 2str.e |
. . . . . . . 8
β’ πΈ = Slot π |
9 | | 2str.n |
. . . . . . . 8
β’ π β β |
10 | 8, 9 | ndxarg 12485 |
. . . . . . 7
β’ (πΈβndx) = π |
11 | 10, 9 | eqeltri 2250 |
. . . . . 6
β’ (πΈβndx) β
β |
12 | 11 | a1i 9 |
. . . . 5
β’ ((π΅ β π β§ + β π) β (πΈβndx) β β) |
13 | | simpr 110 |
. . . . 5
β’ ((π΅ β π β§ + β π) β + β π) |
14 | | opexg 4229 |
. . . . 5
β’ (((πΈβndx) β β β§
+ β
π) β β¨(πΈβndx), + β© β
V) |
15 | 12, 13, 14 | syl2anc 411 |
. . . 4
β’ ((π΅ β π β§ + β π) β β¨(πΈβndx), + β© β
V) |
16 | | prexg 4212 |
. . . 4
β’
((β¨(Baseβndx), π΅β© β V β§ β¨(πΈβndx), + β© β V) β
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} β
V) |
17 | 7, 15, 16 | syl2anc 411 |
. . 3
β’ ((π΅ β π β§ + β π) β {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} β
V) |
18 | 2, 17 | eqeltrid 2264 |
. 2
β’ ((π΅ β π β§ + β π) β πΊ β V) |
19 | 3 | nnrei 8928 |
. . . . . 6
β’
(Baseβndx) β β |
20 | | 2str.l |
. . . . . . 7
β’ 1 <
π |
21 | | basendx 12517 |
. . . . . . 7
β’
(Baseβndx) = 1 |
22 | 20, 21, 10 | 3brtr4i 4034 |
. . . . . 6
β’
(Baseβndx) < (πΈβndx) |
23 | 19, 22 | ltneii 8054 |
. . . . 5
β’
(Baseβndx) β (πΈβndx) |
24 | 23 | a1i 9 |
. . . 4
β’ ((π΅ β π β§ + β π) β (Baseβndx) β (πΈβndx)) |
25 | | funprg 5267 |
. . . 4
β’
((((Baseβndx) β β β§ (πΈβndx) β β) β§ (π΅ β π β§ + β π) β§ (Baseβndx) β (πΈβndx)) β Fun
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
26 | 4, 12, 5, 13, 24, 25 | syl221anc 1249 |
. . 3
β’ ((π΅ β π β§ + β π) β Fun {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
27 | 2 | funeqi 5238 |
. . 3
β’ (Fun
πΊ β Fun
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
28 | 26, 27 | sylibr 134 |
. 2
β’ ((π΅ β π β§ + β π) β Fun πΊ) |
29 | | prid1g 3697 |
. . . 4
β’
(β¨(Baseβndx), π΅β© β V β
β¨(Baseβndx), π΅β© β {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
30 | 7, 29 | syl 14 |
. . 3
β’ ((π΅ β π β§ + β π) β β¨(Baseβndx), π΅β© β
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
31 | 30, 2 | eleqtrrdi 2271 |
. 2
β’ ((π΅ β π β§ + β π) β β¨(Baseβndx), π΅β© β πΊ) |
32 | 1, 18, 28, 31 | strslfvd 12504 |
1
β’ ((π΅ β π β§ + β π) β π΅ = (BaseβπΊ)) |