Step | Hyp | Ref
| Expression |
1 | | isassa.v |
. . . 4
β’ π = (Baseβπ) |
2 | | isassa.f |
. . . 4
β’ πΉ = (Scalarβπ) |
3 | | isassa.b |
. . . 4
β’ π΅ = (BaseβπΉ) |
4 | | isassa.s |
. . . 4
β’ Β· = (
Β·π βπ) |
5 | | isassa.t |
. . . 4
β’ Γ =
(.rβπ) |
6 | 1, 2, 3, 4, 5 | isassa 21278 |
. . 3
β’ (π β AssAlg β ((π β LMod β§ π β Ring β§ πΉ β CRing) β§
βπ β π΅ βπ₯ β π βπ¦ β π (((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β§ (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))))) |
7 | 6 | simprbi 498 |
. 2
β’ (π β AssAlg β
βπ β π΅ βπ₯ β π βπ¦ β π (((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β§ (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦)))) |
8 | | oveq1 7365 |
. . . . . 6
β’ (π = π΄ β (π Β· π₯) = (π΄ Β· π₯)) |
9 | 8 | oveq1d 7373 |
. . . . 5
β’ (π = π΄ β ((π Β· π₯) Γ π¦) = ((π΄ Β· π₯) Γ π¦)) |
10 | | oveq1 7365 |
. . . . 5
β’ (π = π΄ β (π Β· (π₯ Γ π¦)) = (π΄ Β· (π₯ Γ π¦))) |
11 | 9, 10 | eqeq12d 2749 |
. . . 4
β’ (π = π΄ β (((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β ((π΄ Β· π₯) Γ π¦) = (π΄ Β· (π₯ Γ π¦)))) |
12 | | oveq1 7365 |
. . . . . 6
β’ (π = π΄ β (π Β· π¦) = (π΄ Β· π¦)) |
13 | 12 | oveq2d 7374 |
. . . . 5
β’ (π = π΄ β (π₯ Γ (π Β· π¦)) = (π₯ Γ (π΄ Β· π¦))) |
14 | 13, 10 | eqeq12d 2749 |
. . . 4
β’ (π = π΄ β ((π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦)) β (π₯ Γ (π΄ Β· π¦)) = (π΄ Β· (π₯ Γ π¦)))) |
15 | 11, 14 | anbi12d 632 |
. . 3
β’ (π = π΄ β ((((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β§ (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))) β (((π΄ Β· π₯) Γ π¦) = (π΄ Β· (π₯ Γ π¦)) β§ (π₯ Γ (π΄ Β· π¦)) = (π΄ Β· (π₯ Γ π¦))))) |
16 | | oveq2 7366 |
. . . . . 6
β’ (π₯ = π β (π΄ Β· π₯) = (π΄ Β· π)) |
17 | 16 | oveq1d 7373 |
. . . . 5
β’ (π₯ = π β ((π΄ Β· π₯) Γ π¦) = ((π΄ Β· π) Γ π¦)) |
18 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = π β (π₯ Γ π¦) = (π Γ π¦)) |
19 | 18 | oveq2d 7374 |
. . . . 5
β’ (π₯ = π β (π΄ Β· (π₯ Γ π¦)) = (π΄ Β· (π Γ π¦))) |
20 | 17, 19 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β (((π΄ Β· π₯) Γ π¦) = (π΄ Β· (π₯ Γ π¦)) β ((π΄ Β· π) Γ π¦) = (π΄ Β· (π Γ π¦)))) |
21 | | oveq1 7365 |
. . . . 5
β’ (π₯ = π β (π₯ Γ (π΄ Β· π¦)) = (π Γ (π΄ Β· π¦))) |
22 | 21, 19 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β ((π₯ Γ (π΄ Β· π¦)) = (π΄ Β· (π₯ Γ π¦)) β (π Γ (π΄ Β· π¦)) = (π΄ Β· (π Γ π¦)))) |
23 | 20, 22 | anbi12d 632 |
. . 3
β’ (π₯ = π β ((((π΄ Β· π₯) Γ π¦) = (π΄ Β· (π₯ Γ π¦)) β§ (π₯ Γ (π΄ Β· π¦)) = (π΄ Β· (π₯ Γ π¦))) β (((π΄ Β· π) Γ π¦) = (π΄ Β· (π Γ π¦)) β§ (π Γ (π΄ Β· π¦)) = (π΄ Β· (π Γ π¦))))) |
24 | | oveq2 7366 |
. . . . 5
β’ (π¦ = π β ((π΄ Β· π) Γ π¦) = ((π΄ Β· π) Γ π)) |
25 | | oveq2 7366 |
. . . . . 6
β’ (π¦ = π β (π Γ π¦) = (π Γ π)) |
26 | 25 | oveq2d 7374 |
. . . . 5
β’ (π¦ = π β (π΄ Β· (π Γ π¦)) = (π΄ Β· (π Γ π))) |
27 | 24, 26 | eqeq12d 2749 |
. . . 4
β’ (π¦ = π β (((π΄ Β· π) Γ π¦) = (π΄ Β· (π Γ π¦)) β ((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)))) |
28 | | oveq2 7366 |
. . . . . 6
β’ (π¦ = π β (π΄ Β· π¦) = (π΄ Β· π)) |
29 | 28 | oveq2d 7374 |
. . . . 5
β’ (π¦ = π β (π Γ (π΄ Β· π¦)) = (π Γ (π΄ Β· π))) |
30 | 29, 26 | eqeq12d 2749 |
. . . 4
β’ (π¦ = π β ((π Γ (π΄ Β· π¦)) = (π΄ Β· (π Γ π¦)) β (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π)))) |
31 | 27, 30 | anbi12d 632 |
. . 3
β’ (π¦ = π β ((((π΄ Β· π) Γ π¦) = (π΄ Β· (π Γ π¦)) β§ (π Γ (π΄ Β· π¦)) = (π΄ Β· (π Γ π¦))) β (((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)) β§ (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π))))) |
32 | 15, 23, 31 | rspc3v 3592 |
. 2
β’ ((π΄ β π΅ β§ π β π β§ π β π) β (βπ β π΅ βπ₯ β π βπ¦ β π (((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β§ (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))) β (((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)) β§ (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π))))) |
33 | 7, 32 | mpan9 508 |
1
β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β (((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)) β§ (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π)))) |