Step | Hyp | Ref
| Expression |
1 | | 2str.e |
. . 3
β’ πΈ = Slot π |
2 | | 2str.n |
. . 3
β’ π β β |
3 | 1, 2 | ndxslid 12489 |
. 2
β’ (πΈ = Slot (πΈβndx) β§ (πΈβndx) β β) |
4 | | 2str.g |
. . 3
β’ πΊ = {β¨(Baseβndx),
π΅β©, β¨(πΈβndx), + β©} |
5 | | basendxnn 12520 |
. . . . . 6
β’
(Baseβndx) β β |
6 | 5 | a1i 9 |
. . . . 5
β’ ((π΅ β π β§ + β π) β (Baseβndx) β
β) |
7 | | simpl 109 |
. . . . 5
β’ ((π΅ β π β§ + β π) β π΅ β π) |
8 | | opexg 4230 |
. . . . 5
β’
(((Baseβndx) β β β§ π΅ β π) β β¨(Baseβndx), π΅β© β
V) |
9 | 6, 7, 8 | syl2anc 411 |
. . . 4
β’ ((π΅ β π β§ + β π) β β¨(Baseβndx), π΅β© β
V) |
10 | 1, 2 | ndxarg 12487 |
. . . . . . 7
β’ (πΈβndx) = π |
11 | 10, 2 | eqeltri 2250 |
. . . . . 6
β’ (πΈβndx) β
β |
12 | 11 | a1i 9 |
. . . . 5
β’ ((π΅ β π β§ + β π) β (πΈβndx) β β) |
13 | | simpr 110 |
. . . . 5
β’ ((π΅ β π β§ + β π) β + β π) |
14 | | opexg 4230 |
. . . . 5
β’ (((πΈβndx) β β β§
+ β
π) β β¨(πΈβndx), + β© β
V) |
15 | 12, 13, 14 | syl2anc 411 |
. . . 4
β’ ((π΅ β π β§ + β π) β β¨(πΈβndx), + β© β
V) |
16 | | prexg 4213 |
. . . 4
β’
((β¨(Baseβndx), π΅β© β V β§ β¨(πΈβndx), + β© β V) β
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} β
V) |
17 | 9, 15, 16 | syl2anc 411 |
. . 3
β’ ((π΅ β π β§ + β π) β {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} β
V) |
18 | 4, 17 | eqeltrid 2264 |
. 2
β’ ((π΅ β π β§ + β π) β πΊ β V) |
19 | 5 | nnrei 8930 |
. . . . . 6
β’
(Baseβndx) β β |
20 | | 2str.l |
. . . . . . 7
β’ 1 <
π |
21 | | basendx 12519 |
. . . . . . 7
β’
(Baseβndx) = 1 |
22 | 20, 21, 10 | 3brtr4i 4035 |
. . . . . 6
β’
(Baseβndx) < (πΈβndx) |
23 | 19, 22 | ltneii 8056 |
. . . . 5
β’
(Baseβndx) β (πΈβndx) |
24 | 23 | a1i 9 |
. . . 4
β’ ((π΅ β π β§ + β π) β (Baseβndx) β (πΈβndx)) |
25 | | funprg 5268 |
. . . 4
β’
((((Baseβndx) β β β§ (πΈβndx) β β) β§ (π΅ β π β§ + β π) β§ (Baseβndx) β (πΈβndx)) β Fun
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
26 | 6, 12, 7, 13, 24, 25 | syl221anc 1249 |
. . 3
β’ ((π΅ β π β§ + β π) β Fun {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
27 | 4 | funeqi 5239 |
. . 3
β’ (Fun
πΊ β Fun
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
28 | 26, 27 | sylibr 134 |
. 2
β’ ((π΅ β π β§ + β π) β Fun πΊ) |
29 | | prid2g 3699 |
. . . 4
β’
(β¨(πΈβndx), + β© β V β
β¨(πΈβndx), + β© β
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
30 | 15, 29 | syl 14 |
. . 3
β’ ((π΅ β π β§ + β π) β β¨(πΈβndx), + β© β
{β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©}) |
31 | 30, 4 | eleqtrrdi 2271 |
. 2
β’ ((π΅ β π β§ + β π) β β¨(πΈβndx), + β© β πΊ) |
32 | 3, 18, 28, 31 | strslfvd 12506 |
1
β’ ((π΅ β π β§ + β π) β + = (πΈβπΊ)) |