Step | Hyp | Ref
| Expression |
1 | | vciOLD.1 |
. . . . 5
β’ πΊ = (1st βπ) |
2 | 1 | eqeq2i 2746 |
. . . 4
β’ (π = πΊ β π = (1st βπ)) |
3 | | eleq1 2822 |
. . . . 5
β’ (π = πΊ β (π β AbelOp β πΊ β AbelOp)) |
4 | | rneq 5892 |
. . . . . . 7
β’ (π = πΊ β ran π = ran πΊ) |
5 | | vciOLD.3 |
. . . . . . 7
β’ π = ran πΊ |
6 | 4, 5 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΊ β ran π = π) |
7 | | xpeq2 5655 |
. . . . . . . 8
β’ (ran
π = π β (β Γ ran π) = (β Γ π)) |
8 | 7 | feq2d 6655 |
. . . . . . 7
β’ (ran
π = π β (π :(β Γ ran π)βΆran π β π :(β Γ π)βΆran π)) |
9 | | feq3 6652 |
. . . . . . 7
β’ (ran
π = π β (π :(β Γ π)βΆran π β π :(β Γ π)βΆπ)) |
10 | 8, 9 | bitrd 279 |
. . . . . 6
β’ (ran
π = π β (π :(β Γ ran π)βΆran π β π :(β Γ π)βΆπ)) |
11 | 6, 10 | syl 17 |
. . . . 5
β’ (π = πΊ β (π :(β Γ ran π)βΆran π β π :(β Γ π)βΆπ)) |
12 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (π = πΊ β (π₯ππ§) = (π₯πΊπ§)) |
13 | 12 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = πΊ β (π¦π (π₯ππ§)) = (π¦π (π₯πΊπ§))) |
14 | | oveq 7364 |
. . . . . . . . . . 11
β’ (π = πΊ β ((π¦π π₯)π(π¦π π§)) = ((π¦π π₯)πΊ(π¦π π§))) |
15 | 13, 14 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π = πΊ β ((π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)))) |
16 | 6, 15 | raleqbidv 3318 |
. . . . . . . . 9
β’ (π = πΊ β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)))) |
17 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (π = πΊ β ((π¦π π₯)π(π§π π₯)) = ((π¦π π₯)πΊ(π§π π₯))) |
18 | 17 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π = πΊ β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β ((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)))) |
19 | 18 | anbi1d 631 |
. . . . . . . . . 10
β’ (π = πΊ β ((((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))) β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))) |
20 | 19 | ralbidv 3171 |
. . . . . . . . 9
β’ (π = πΊ β (βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))) β βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))) |
21 | 16, 20 | anbi12d 632 |
. . . . . . . 8
β’ (π = πΊ β ((βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))) β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))) |
22 | 21 | ralbidv 3171 |
. . . . . . 7
β’ (π = πΊ β (βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))) β βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))) |
23 | 22 | anbi2d 630 |
. . . . . 6
β’ (π = πΊ β (((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))) β ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))))) |
24 | 6, 23 | raleqbidv 3318 |
. . . . 5
β’ (π = πΊ β (βπ₯ β ran π((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))) β βπ₯ β π ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))))) |
25 | 3, 11, 24 | 3anbi123d 1437 |
. . . 4
β’ (π = πΊ β ((π β AbelOp β§ π :(β Γ ran π)βΆran π β§ βπ₯ β ran π((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))) β (πΊ β AbelOp β§ π :(β Γ π)βΆπ β§ βπ₯ β π ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))))) |
26 | 2, 25 | sylbir 234 |
. . 3
β’ (π = (1st βπ) β ((π β AbelOp β§ π :(β Γ ran π)βΆran π β§ βπ₯ β ran π((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))) β (πΊ β AbelOp β§ π :(β Γ π)βΆπ β§ βπ₯ β π ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))))) |
27 | | vciOLD.2 |
. . . . 5
β’ π = (2nd βπ) |
28 | 27 | eqeq2i 2746 |
. . . 4
β’ (π = π β π = (2nd βπ)) |
29 | | feq1 6650 |
. . . . 5
β’ (π = π β (π :(β Γ π)βΆπ β π:(β Γ π)βΆπ)) |
30 | | oveq 7364 |
. . . . . . . 8
β’ (π = π β (1π π₯) = (1ππ₯)) |
31 | 30 | eqeq1d 2735 |
. . . . . . 7
β’ (π = π β ((1π π₯) = π₯ β (1ππ₯) = π₯)) |
32 | | oveq 7364 |
. . . . . . . . . . 11
β’ (π = π β (π¦π (π₯πΊπ§)) = (π¦π(π₯πΊπ§))) |
33 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (π = π β (π¦π π₯) = (π¦ππ₯)) |
34 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (π = π β (π¦π π§) = (π¦ππ§)) |
35 | 33, 34 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (π = π β ((π¦π π₯)πΊ(π¦π π§)) = ((π¦ππ₯)πΊ(π¦ππ§))) |
36 | 32, 35 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π = π β ((π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)))) |
37 | 36 | ralbidv 3171 |
. . . . . . . . 9
β’ (π = π β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)))) |
38 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (π = π β ((π¦ + π§)π π₯) = ((π¦ + π§)ππ₯)) |
39 | | oveq 7364 |
. . . . . . . . . . . . 13
β’ (π = π β (π§π π₯) = (π§ππ₯)) |
40 | 33, 39 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = π β ((π¦π π₯)πΊ(π§π π₯)) = ((π¦ππ₯)πΊ(π§ππ₯))) |
41 | 38, 40 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π = π β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β ((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)))) |
42 | | oveq 7364 |
. . . . . . . . . . . 12
β’ (π = π β ((π¦ Β· π§)π π₯) = ((π¦ Β· π§)ππ₯)) |
43 | 39 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π = π β (π¦π (π§π π₯)) = (π¦π (π§ππ₯))) |
44 | | oveq 7364 |
. . . . . . . . . . . . 13
β’ (π = π β (π¦π (π§ππ₯)) = (π¦π(π§ππ₯))) |
45 | 43, 44 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π = π β (π¦π (π§π π₯)) = (π¦π(π§ππ₯))) |
46 | 42, 45 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π = π β (((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)) β ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯)))) |
47 | 41, 46 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = π β ((((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))) β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯))))) |
48 | 47 | ralbidv 3171 |
. . . . . . . . 9
β’ (π = π β (βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))) β βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯))))) |
49 | 37, 48 | anbi12d 632 |
. . . . . . . 8
β’ (π = π β ((βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))) β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯)))))) |
50 | 49 | ralbidv 3171 |
. . . . . . 7
β’ (π = π β (βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))) β βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯)))))) |
51 | 31, 50 | anbi12d 632 |
. . . . . 6
β’ (π = π β (((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))) β ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯))))))) |
52 | 51 | ralbidv 3171 |
. . . . 5
β’ (π = π β (βπ₯ β π ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))) β βπ₯ β π ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯))))))) |
53 | 29, 52 | 3anbi23d 1440 |
. . . 4
β’ (π = π β ((πΊ β AbelOp β§ π :(β Γ π)βΆπ β§ βπ₯ β π ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))) β (πΊ β AbelOp β§ π:(β Γ π)βΆπ β§ βπ₯ β π ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯)))))))) |
54 | 28, 53 | sylbir 234 |
. . 3
β’ (π = (2nd βπ) β ((πΊ β AbelOp β§ π :(β Γ π)βΆπ β§ βπ₯ β π ((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π (π₯πΊπ§)) = ((π¦π π₯)πΊ(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)πΊ(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯)))))) β (πΊ β AbelOp β§ π:(β Γ π)βΆπ β§ βπ₯ β π ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯)))))))) |
55 | 26, 54 | elopabi 7995 |
. 2
β’ (π β {β¨π, π β© β£ (π β AbelOp β§ π :(β Γ ran π)βΆran π β§ βπ₯ β ran π((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))))} β (πΊ β AbelOp β§ π:(β Γ π)βΆπ β§ βπ₯ β π ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯))))))) |
56 | | df-vc 29543 |
. 2
β’
CVecOLD = {β¨π, π β© β£ (π β AbelOp β§ π :(β Γ ran π)βΆran π β§ βπ₯ β ran π((1π π₯) = π₯ β§ βπ¦ β β (βπ§ β ran π(π¦π (π₯ππ§)) = ((π¦π π₯)π(π¦π π§)) β§ βπ§ β β (((π¦ + π§)π π₯) = ((π¦π π₯)π(π§π π₯)) β§ ((π¦ Β· π§)π π₯) = (π¦π (π§π π₯))))))} |
57 | 55, 56 | eleq2s 2852 |
1
β’ (π β CVecOLD
β (πΊ β AbelOp
β§ π:(β Γ
π)βΆπ β§ βπ₯ β π ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯))))))) |