Step | Hyp | Ref
| Expression |
1 | | rmodislmod.r |
. . . . 5
β’ (π
β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) |
2 | | simprl 770 |
. . . . . . . . 9
β’ ((((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π)) |
3 | 2 | 2ralimi 3124 |
. . . . . . . 8
β’
(βπ₯ β
π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β βπ₯ β π βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π)) |
4 | 3 | 2ralimi 3124 |
. . . . . . 7
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π)) |
5 | | ralrot3 3291 |
. . . . . . . . 9
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β βπ₯ β π βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π)) |
6 | | rmodislmod.v |
. . . . . . . . . . . . . 14
β’ π = (Baseβπ
) |
7 | 6 | grpbn0 18848 |
. . . . . . . . . . . . 13
β’ (π
β Grp β π β β
) |
8 | 7 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π
β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) β π β β
) |
9 | 1, 8 | ax-mp 5 |
. . . . . . . . . . 11
β’ π β β
|
10 | | rspn0 4352 |
. . . . . . . . . . 11
β’ (π β β
β
(βπ₯ β π βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π))) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . 10
β’
(βπ₯ β
π βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π)) |
12 | | oveq1 7413 |
. . . . . . . . . . . . . 14
β’ (π = π β (π Γ π) = (π Γ π)) |
13 | 12 | oveq2d 7422 |
. . . . . . . . . . . . 13
β’ (π = π β (π€ Β· (π Γ π)) = (π€ Β· (π Γ π))) |
14 | | oveq2 7414 |
. . . . . . . . . . . . . 14
β’ (π = π β (π€ Β· π) = (π€ Β· π)) |
15 | 14 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ (π = π β ((π€ Β· π) Β· π) = ((π€ Β· π) Β· π)) |
16 | 13, 15 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π = π β ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π))) |
17 | | oveq2 7414 |
. . . . . . . . . . . . . 14
β’ (π = π β (π Γ π) = (π Γ π)) |
18 | 17 | oveq2d 7422 |
. . . . . . . . . . . . 13
β’ (π = π β (π€ Β· (π Γ π)) = (π€ Β· (π Γ π))) |
19 | | oveq2 7414 |
. . . . . . . . . . . . 13
β’ (π = π β ((π€ Β· π) Β· π) = ((π€ Β· π) Β· π)) |
20 | 18, 19 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π = π β ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π))) |
21 | | oveq1 7413 |
. . . . . . . . . . . . 13
β’ (π€ = π β (π€ Β· (π Γ π)) = (π Β· (π Γ π))) |
22 | | oveq1 7413 |
. . . . . . . . . . . . . 14
β’ (π€ = π β (π€ Β· π) = (π Β· π)) |
23 | 22 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ (π€ = π β ((π€ Β· π) Β· π) = ((π Β· π) Β· π)) |
24 | 21, 23 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π€ = π β ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β (π Β· (π Γ π)) = ((π Β· π) Β· π))) |
25 | 16, 20, 24 | rspc3v 3627 |
. . . . . . . . . . 11
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β (π Β· (π Γ π)) = ((π Β· π) Β· π))) |
26 | 25 | 3com12 1124 |
. . . . . . . . . 10
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β (π Β· (π Γ π)) = ((π Β· π) Β· π))) |
27 | 11, 26 | syl5com 31 |
. . . . . . . . 9
β’
(βπ₯ β
π βπ β πΎ βπ β πΎ βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β ((π β πΎ β§ π β πΎ β§ π β π) β (π Β· (π Γ π)) = ((π Β· π) Β· π))) |
28 | 5, 27 | sylbi 216 |
. . . . . . . 8
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β ((π β πΎ β§ π β πΎ β§ π β π) β (π Β· (π Γ π)) = ((π Β· π) Β· π))) |
29 | | eqcom 2740 |
. . . . . . . 8
β’ (((π Β· π) Β· π) = (π Β· (π Γ π)) β (π Β· (π Γ π)) = ((π Β· π) Β· π)) |
30 | 28, 29 | syl6ibr 252 |
. . . . . . 7
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β ((π β πΎ β§ π β πΎ β§ π β π) β ((π Β· π) Β· π) = (π Β· (π Γ π)))) |
31 | 4, 30 | syl 17 |
. . . . . 6
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β ((π β πΎ β§ π β πΎ β§ π β π) β ((π Β· π) Β· π) = (π Β· (π Γ π)))) |
32 | 31 | 3ad2ant3 1136 |
. . . . 5
β’ ((π
β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) β ((π β πΎ β§ π β πΎ β§ π β π) β ((π Β· π) Β· π) = (π Β· (π Γ π)))) |
33 | 1, 32 | ax-mp 5 |
. . . 4
β’ ((π β πΎ β§ π β πΎ β§ π β π) β ((π Β· π) Β· π) = (π Β· (π Γ π))) |
34 | 33 | adantl 483 |
. . 3
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Β· π) Β· π) = (π Β· (π Γ π))) |
35 | | rmodislmod.k |
. . . . . . . . . 10
β’ πΎ = (BaseβπΉ) |
36 | | rmodislmod.t |
. . . . . . . . . 10
β’ Γ =
(.rβπΉ) |
37 | 35, 36 | crngcom 20068 |
. . . . . . . . 9
β’ ((πΉ β CRing β§ π β πΎ β§ π β πΎ) β (π Γ π) = (π Γ π)) |
38 | 37 | 3expb 1121 |
. . . . . . . 8
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ)) β (π Γ π) = (π Γ π)) |
39 | 38 | expcom 415 |
. . . . . . 7
β’ ((π β πΎ β§ π β πΎ) β (πΉ β CRing β (π Γ π) = (π Γ π))) |
40 | 39 | ancoms 460 |
. . . . . 6
β’ ((π β πΎ β§ π β πΎ) β (πΉ β CRing β (π Γ π) = (π Γ π))) |
41 | 40 | 3adant3 1133 |
. . . . 5
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (πΉ β CRing β (π Γ π) = (π Γ π))) |
42 | 41 | impcom 409 |
. . . 4
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β (π Γ π) = (π Γ π)) |
43 | 42 | oveq2d 7422 |
. . 3
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β (π Β· (π Γ π)) = (π Β· (π Γ π))) |
44 | 34, 43 | eqtrd 2773 |
. 2
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Β· π) Β· π) = (π Β· (π Γ π))) |
45 | | rmodislmod.m |
. . . . . . 7
β’ β =
(π β πΎ, π£ β π β¦ (π£ Β· π )) |
46 | 45 | a1i 11 |
. . . . . 6
β’ ((π β πΎ β§ π β πΎ β§ π β π) β β = (π β πΎ, π£ β π β¦ (π£ Β· π ))) |
47 | | oveq12 7415 |
. . . . . . . 8
β’ ((π£ = π β§ π = π) β (π£ Β· π ) = (π Β· π)) |
48 | 47 | ancoms 460 |
. . . . . . 7
β’ ((π = π β§ π£ = π) β (π£ Β· π ) = (π Β· π)) |
49 | 48 | adantl 483 |
. . . . . 6
β’ (((π β πΎ β§ π β πΎ β§ π β π) β§ (π = π β§ π£ = π)) β (π£ Β· π ) = (π Β· π)) |
50 | | simp2 1138 |
. . . . . 6
β’ ((π β πΎ β§ π β πΎ β§ π β π) β π β πΎ) |
51 | | simp3 1139 |
. . . . . 6
β’ ((π β πΎ β§ π β πΎ β§ π β π) β π β π) |
52 | | ovexd 7441 |
. . . . . 6
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π Β· π) β V) |
53 | 46, 49, 50, 51, 52 | ovmpod 7557 |
. . . . 5
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π β π) = (π Β· π)) |
54 | 53 | oveq2d 7422 |
. . . 4
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π β (π β π)) = (π β (π Β· π))) |
55 | | oveq12 7415 |
. . . . . . 7
β’ ((π£ = (π Β· π) β§ π = π) β (π£ Β· π ) = ((π Β· π) Β· π)) |
56 | 55 | ancoms 460 |
. . . . . 6
β’ ((π = π β§ π£ = (π Β· π)) β (π£ Β· π ) = ((π Β· π) Β· π)) |
57 | 56 | adantl 483 |
. . . . 5
β’ (((π β πΎ β§ π β πΎ β§ π β π) β§ (π = π β§ π£ = (π Β· π))) β (π£ Β· π ) = ((π Β· π) Β· π)) |
58 | | simp1 1137 |
. . . . 5
β’ ((π β πΎ β§ π β πΎ β§ π β π) β π β πΎ) |
59 | | simpl1 1192 |
. . . . . . . . . . 11
β’ ((((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β (π€ Β· π) β π) |
60 | 59 | 2ralimi 3124 |
. . . . . . . . . 10
β’
(βπ₯ β
π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β βπ₯ β π βπ€ β π (π€ Β· π) β π) |
61 | 60 | 2ralimi 3124 |
. . . . . . . . 9
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π) |
62 | | ringgrp 20055 |
. . . . . . . . . . . . 13
β’ (πΉ β Ring β πΉ β Grp) |
63 | 35 | grpbn0 18848 |
. . . . . . . . . . . . 13
β’ (πΉ β Grp β πΎ β β
) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ β Ring β πΎ β β
) |
65 | 64 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π
β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) β πΎ β β
) |
66 | 1, 65 | ax-mp 5 |
. . . . . . . . . 10
β’ πΎ β β
|
67 | | rspn0 4352 |
. . . . . . . . . 10
β’ (πΎ β β
β
(βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π β βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π)) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π β βπ β πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π) |
69 | | ralcom 3287 |
. . . . . . . . . 10
β’
(βπ β
πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π β βπ₯ β π βπ β πΎ βπ€ β π (π€ Β· π) β π) |
70 | | rspn0 4352 |
. . . . . . . . . . . 12
β’ (π β β
β
(βπ₯ β π βπ β πΎ βπ€ β π (π€ Β· π) β π β βπ β πΎ βπ€ β π (π€ Β· π) β π)) |
71 | 9, 70 | ax-mp 5 |
. . . . . . . . . . 11
β’
(βπ₯ β
π βπ β πΎ βπ€ β π (π€ Β· π) β π β βπ β πΎ βπ€ β π (π€ Β· π) β π) |
72 | | oveq2 7414 |
. . . . . . . . . . . . 13
β’ (π = π β (π€ Β· π) = (π€ Β· π)) |
73 | 72 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π β ((π€ Β· π) β π β (π€ Β· π) β π)) |
74 | 22 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π€ = π β ((π€ Β· π) β π β (π Β· π) β π)) |
75 | 73, 74 | rspc2v 3622 |
. . . . . . . . . . 11
β’ ((π β πΎ β§ π β π) β (βπ β πΎ βπ€ β π (π€ Β· π) β π β (π Β· π) β π)) |
76 | 71, 75 | syl5com 31 |
. . . . . . . . . 10
β’
(βπ₯ β
π βπ β πΎ βπ€ β π (π€ Β· π) β π β ((π β πΎ β§ π β π) β (π Β· π) β π)) |
77 | 69, 76 | sylbi 216 |
. . . . . . . . 9
β’
(βπ β
πΎ βπ₯ β π βπ€ β π (π€ Β· π) β π β ((π β πΎ β§ π β π) β (π Β· π) β π)) |
78 | 61, 68, 77 | 3syl 18 |
. . . . . . . 8
β’
(βπ β
πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€)) β ((π β πΎ β§ π β π) β (π Β· π) β π)) |
79 | 78 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π
β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) β ((π β πΎ β§ π β π) β (π Β· π) β π)) |
80 | 1, 79 | ax-mp 5 |
. . . . . 6
β’ ((π β πΎ β§ π β π) β (π Β· π) β π) |
81 | 80 | 3adant1 1131 |
. . . . 5
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π Β· π) β π) |
82 | | ovexd 7441 |
. . . . 5
β’ ((π β πΎ β§ π β πΎ β§ π β π) β ((π Β· π) Β· π) β V) |
83 | 46, 57, 58, 81, 82 | ovmpod 7557 |
. . . 4
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π β (π Β· π)) = ((π Β· π) Β· π)) |
84 | 54, 83 | eqtrd 2773 |
. . 3
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π β (π β π)) = ((π Β· π) Β· π)) |
85 | 84 | adantl 483 |
. 2
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β (π β (π β π)) = ((π Β· π) Β· π)) |
86 | | oveq12 7415 |
. . . . . 6
β’ ((π£ = π β§ π = (π Γ π)) β (π£ Β· π ) = (π Β· (π Γ π))) |
87 | 86 | ancoms 460 |
. . . . 5
β’ ((π = (π Γ π) β§ π£ = π) β (π£ Β· π ) = (π Β· (π Γ π))) |
88 | 87 | adantl 483 |
. . . 4
β’ (((π β πΎ β§ π β πΎ β§ π β π) β§ (π = (π Γ π) β§ π£ = π)) β (π£ Β· π ) = (π Β· (π Γ π))) |
89 | 35, 36 | ringcl 20067 |
. . . . . . . 8
β’ ((πΉ β Ring β§ π β πΎ β§ π β πΎ) β (π Γ π) β πΎ) |
90 | 89 | 3expib 1123 |
. . . . . . 7
β’ (πΉ β Ring β ((π β πΎ β§ π β πΎ) β (π Γ π) β πΎ)) |
91 | 90 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π
β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π€ Β· π) β π β§ ((π€ + π₯) Β· π) = ((π€ Β· π) + (π₯ Β· π)) β§ (π€ Β· (π ⨣ π)) = ((π€ Β· π) + (π€ Β· π))) β§ ((π€ Β· (π Γ π)) = ((π€ Β· π) Β· π) β§ (π€ Β· 1 ) = π€))) β ((π β πΎ β§ π β πΎ) β (π Γ π) β πΎ)) |
92 | 1, 91 | ax-mp 5 |
. . . . 5
β’ ((π β πΎ β§ π β πΎ) β (π Γ π) β πΎ) |
93 | 92 | 3adant3 1133 |
. . . 4
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π Γ π) β πΎ) |
94 | | ovexd 7441 |
. . . 4
β’ ((π β πΎ β§ π β πΎ β§ π β π) β (π Β· (π Γ π)) β V) |
95 | 46, 88, 93, 51, 94 | ovmpod 7557 |
. . 3
β’ ((π β πΎ β§ π β πΎ β§ π β π) β ((π Γ π) β π) = (π Β· (π Γ π))) |
96 | 95 | adantl 483 |
. 2
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Γ π) β π) = (π Β· (π Γ π))) |
97 | 44, 85, 96 | 3eqtr4rd 2784 |
1
β’ ((πΉ β CRing β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Γ π) β π) = (π β (π β π))) |