Step | Hyp | Ref
| Expression |
1 | | xpider 8733 |
. 2
β’ (π Γ π) Er π |
2 | | simpll 766 |
. . . . 5
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β π₯ β π) |
3 | | efgval.w |
. . . . . . . . 9
β’ π = ( I βWord (πΌ Γ
2o)) |
4 | | fviss 6922 |
. . . . . . . . 9
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
5 | 3, 4 | eqsstri 3982 |
. . . . . . . 8
β’ π β Word (πΌ Γ 2o) |
6 | 5, 2 | sselid 3946 |
. . . . . . 7
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β π₯ β Word (πΌ Γ 2o)) |
7 | | opelxpi 5674 |
. . . . . . . . 9
β’ ((π¦ β πΌ β§ π§ β 2o) β β¨π¦, π§β© β (πΌ Γ 2o)) |
8 | 7 | adantl 483 |
. . . . . . . 8
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β β¨π¦, π§β© β (πΌ Γ 2o)) |
9 | | 2oconcl 8453 |
. . . . . . . . . 10
β’ (π§ β 2o β
(1o β π§)
β 2o) |
10 | | opelxpi 5674 |
. . . . . . . . . 10
β’ ((π¦ β πΌ β§ (1o β π§) β 2o) β
β¨π¦, (1o
β π§)β© β
(πΌ Γ
2o)) |
11 | 9, 10 | sylan2 594 |
. . . . . . . . 9
β’ ((π¦ β πΌ β§ π§ β 2o) β β¨π¦, (1o β π§)β© β (πΌ Γ
2o)) |
12 | 11 | adantl 483 |
. . . . . . . 8
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β β¨π¦, (1o β π§)β© β (πΌ Γ
2o)) |
13 | 8, 12 | s2cld 14769 |
. . . . . . 7
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β
β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ© β Word (πΌ Γ
2o)) |
14 | | splcl 14649 |
. . . . . . 7
β’ ((π₯ β Word (πΌ Γ 2o) β§
β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ© β Word (πΌ Γ 2o)) β
(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β Word
(πΌ Γ
2o)) |
15 | 6, 13, 14 | syl2anc 585 |
. . . . . 6
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β (π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β Word
(πΌ Γ
2o)) |
16 | 3 | efgrcl 19505 |
. . . . . . . 8
β’ (π₯ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
17 | 16 | simprd 497 |
. . . . . . 7
β’ (π₯ β π β π = Word (πΌ Γ 2o)) |
18 | 17 | ad2antrr 725 |
. . . . . 6
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β π = Word (πΌ Γ 2o)) |
19 | 15, 18 | eleqtrrd 2837 |
. . . . 5
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β (π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β π) |
20 | | brxp 5685 |
. . . . 5
β’ (π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β (π₯ β π β§ (π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β π)) |
21 | 2, 19, 20 | sylanbrc 584 |
. . . 4
β’ (((π₯ β π β§ π β (0...(β―βπ₯))) β§ (π¦ β πΌ β§ π§ β 2o)) β π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) |
22 | 21 | ralrimivva 3194 |
. . 3
β’ ((π₯ β π β§ π β (0...(β―βπ₯))) β βπ¦ β πΌ βπ§ β 2o π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) |
23 | 22 | rgen2 3191 |
. 2
β’
βπ₯ β
π βπ β
(0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) |
24 | 3 | fvexi 6860 |
. . . 4
β’ π β V |
25 | 24, 24 | xpex 7691 |
. . 3
β’ (π Γ π) β V |
26 | | ereq1 8661 |
. . . 4
β’ (π = (π Γ π) β (π Er π β (π Γ π) Er π)) |
27 | | breq 5111 |
. . . . . 6
β’ (π = (π Γ π) β (π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
28 | 27 | 2ralbidv 3209 |
. . . . 5
β’ (π = (π Γ π) β (βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β
βπ¦ β πΌ βπ§ β 2o π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
29 | 28 | 2ralbidv 3209 |
. . . 4
β’ (π = (π Γ π) β (βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β
βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
30 | 26, 29 | anbi12d 632 |
. . 3
β’ (π = (π Γ π) β ((π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β ((π Γ π) Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)))) |
31 | 25, 30 | spcev 3567 |
. 2
β’ (((π Γ π) Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯(π Γ π)(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β
βπ(π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
32 | 1, 23, 31 | mp2an 691 |
1
β’
βπ(π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) |