Step | Hyp | Ref
| Expression |
1 | | casa 21404 |
. 2
class
AssAlg |
2 | | vr |
. . . . . . . . . . . . . 14
setvar π |
3 | 2 | cv 1540 |
. . . . . . . . . . . . 13
class π |
4 | | vx |
. . . . . . . . . . . . . 14
setvar π₯ |
5 | 4 | cv 1540 |
. . . . . . . . . . . . 13
class π₯ |
6 | | vs |
. . . . . . . . . . . . . 14
setvar π |
7 | 6 | cv 1540 |
. . . . . . . . . . . . 13
class π |
8 | 3, 5, 7 | co 7408 |
. . . . . . . . . . . 12
class (ππ π₯) |
9 | | vy |
. . . . . . . . . . . . 13
setvar π¦ |
10 | 9 | cv 1540 |
. . . . . . . . . . . 12
class π¦ |
11 | | vt |
. . . . . . . . . . . . 13
setvar π‘ |
12 | 11 | cv 1540 |
. . . . . . . . . . . 12
class π‘ |
13 | 8, 10, 12 | co 7408 |
. . . . . . . . . . 11
class ((ππ π₯)π‘π¦) |
14 | 5, 10, 12 | co 7408 |
. . . . . . . . . . . 12
class (π₯π‘π¦) |
15 | 3, 14, 7 | co 7408 |
. . . . . . . . . . 11
class (ππ (π₯π‘π¦)) |
16 | 13, 15 | wceq 1541 |
. . . . . . . . . 10
wff ((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) |
17 | 3, 10, 7 | co 7408 |
. . . . . . . . . . . 12
class (ππ π¦) |
18 | 5, 17, 12 | co 7408 |
. . . . . . . . . . 11
class (π₯π‘(ππ π¦)) |
19 | 18, 15 | wceq 1541 |
. . . . . . . . . 10
wff (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦)) |
20 | 16, 19 | wa 396 |
. . . . . . . . 9
wff (((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
21 | | vw |
. . . . . . . . . . 11
setvar π€ |
22 | 21 | cv 1540 |
. . . . . . . . . 10
class π€ |
23 | | cmulr 17197 |
. . . . . . . . . 10
class
.r |
24 | 22, 23 | cfv 6543 |
. . . . . . . . 9
class
(.rβπ€) |
25 | 20, 11, 24 | wsbc 3777 |
. . . . . . . 8
wff
[(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
26 | | cvsca 17200 |
. . . . . . . . 9
class
Β·π |
27 | 22, 26 | cfv 6543 |
. . . . . . . 8
class (
Β·π βπ€) |
28 | 25, 6, 27 | wsbc 3777 |
. . . . . . 7
wff [(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
29 | | cbs 17143 |
. . . . . . . 8
class
Base |
30 | 22, 29 | cfv 6543 |
. . . . . . 7
class
(Baseβπ€) |
31 | 28, 9, 30 | wral 3061 |
. . . . . 6
wff
βπ¦ β
(Baseβπ€)[(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
32 | 31, 4, 30 | wral 3061 |
. . . . 5
wff
βπ₯ β
(Baseβπ€)βπ¦ β (Baseβπ€)[(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
33 | | vf |
. . . . . . 7
setvar π |
34 | 33 | cv 1540 |
. . . . . 6
class π |
35 | 34, 29 | cfv 6543 |
. . . . 5
class
(Baseβπ) |
36 | 32, 2, 35 | wral 3061 |
. . . 4
wff
βπ β
(Baseβπ)βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)[(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
37 | | csca 17199 |
. . . . 5
class
Scalar |
38 | 22, 37 | cfv 6543 |
. . . 4
class
(Scalarβπ€) |
39 | 36, 33, 38 | wsbc 3777 |
. . 3
wff
[(Scalarβπ€) / π]βπ β (Baseβπ)βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)[(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦))) |
40 | | clmod 20470 |
. . . 4
class
LMod |
41 | | crg 20055 |
. . . 4
class
Ring |
42 | 40, 41 | cin 3947 |
. . 3
class (LMod
β© Ring) |
43 | 39, 21, 42 | crab 3432 |
. 2
class {π€ β (LMod β© Ring)
β£ [(Scalarβπ€) / π]βπ β (Baseβπ)βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)[(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦)))} |
44 | 1, 43 | wceq 1541 |
1
wff AssAlg =
{π€ β (LMod β© Ring)
β£ [(Scalarβπ€) / π]βπ β (Baseβπ)βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)[(
Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦)))} |