Step | Hyp | Ref
| Expression |
1 | | lmodgrp 20470 |
. . . 4
β’ (πΎ β LMod β πΎ β Grp) |
2 | 1 | a1i 11 |
. . 3
β’ (π β (πΎ β LMod β πΎ β Grp)) |
3 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
4 | | eqid 2732 |
. . . . . 6
β’
(+gβπΎ) = (+gβπΎ) |
5 | | eqid 2732 |
. . . . . 6
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
6 | | lmodprop2d.f |
. . . . . 6
β’ πΉ = (ScalarβπΎ) |
7 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΉ) =
(BaseβπΉ) |
8 | | eqid 2732 |
. . . . . 6
β’
(+gβπΉ) = (+gβπΉ) |
9 | | eqid 2732 |
. . . . . 6
β’
(.rβπΉ) = (.rβπΉ) |
10 | | eqid 2732 |
. . . . . 6
β’
(1rβπΉ) = (1rβπΉ) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | islmod 20467 |
. . . . 5
β’ (πΎ β LMod β (πΎ β Grp β§ πΉ β Ring β§ βπ β (BaseβπΉ)βπ β (BaseβπΉ)βπ§ β (BaseβπΎ)βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)))) |
12 | 11 | simp2bi 1146 |
. . . 4
β’ (πΎ β LMod β πΉ β Ring) |
13 | 12 | a1i 11 |
. . 3
β’ (π β (πΎ β LMod β πΉ β Ring)) |
14 | | simplr 767 |
. . . . . . 7
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β πΎ β LMod) |
15 | | simprl 769 |
. . . . . . . 8
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π₯ β π) |
16 | | lmodprop2d.p1 |
. . . . . . . . 9
β’ (π β π = (BaseβπΉ)) |
17 | 16 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π = (BaseβπΉ)) |
18 | 15, 17 | eleqtrd 2835 |
. . . . . . 7
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π₯ β (BaseβπΉ)) |
19 | | simprr 771 |
. . . . . . . 8
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π¦ β π΅) |
20 | | lmodprop2d.b1 |
. . . . . . . . 9
β’ (π β π΅ = (BaseβπΎ)) |
21 | 20 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π΅ = (BaseβπΎ)) |
22 | 19, 21 | eleqtrd 2835 |
. . . . . . 7
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π¦ β (BaseβπΎ)) |
23 | 3, 6, 5, 7 | lmodvscl 20481 |
. . . . . . 7
β’ ((πΎ β LMod β§ π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΎ)) β (π₯( Β·π
βπΎ)π¦) β (BaseβπΎ)) |
24 | 14, 18, 22, 23 | syl3anc 1371 |
. . . . . 6
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β (BaseβπΎ)) |
25 | 24, 21 | eleqtrrd 2836 |
. . . . 5
β’ (((π β§ πΎ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β π΅) |
26 | 25 | ralrimivva 3200 |
. . . 4
β’ ((π β§ πΎ β LMod) β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) |
27 | 26 | ex 413 |
. . 3
β’ (π β (πΎ β LMod β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) |
28 | 2, 13, 27 | 3jcad 1129 |
. 2
β’ (π β (πΎ β LMod β (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅))) |
29 | | lmodgrp 20470 |
. . . 4
β’ (πΏ β LMod β πΏ β Grp) |
30 | | lmodprop2d.b2 |
. . . . 5
β’ (π β π΅ = (BaseβπΏ)) |
31 | | lmodprop2d.1 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
32 | 20, 30, 31 | grppropd 18833 |
. . . 4
β’ (π β (πΎ β Grp β πΏ β Grp)) |
33 | 29, 32 | imbitrrid 245 |
. . 3
β’ (π β (πΏ β LMod β πΎ β Grp)) |
34 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΏ) =
(BaseβπΏ) |
35 | | eqid 2732 |
. . . . . 6
β’
(+gβπΏ) = (+gβπΏ) |
36 | | eqid 2732 |
. . . . . 6
β’ (
Β·π βπΏ) = ( Β·π
βπΏ) |
37 | | lmodprop2d.g |
. . . . . 6
β’ πΊ = (ScalarβπΏ) |
38 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
39 | | eqid 2732 |
. . . . . 6
β’
(+gβπΊ) = (+gβπΊ) |
40 | | eqid 2732 |
. . . . . 6
β’
(.rβπΊ) = (.rβπΊ) |
41 | | eqid 2732 |
. . . . . 6
β’
(1rβπΊ) = (1rβπΊ) |
42 | 34, 35, 36, 37, 38, 39, 40, 41 | islmod 20467 |
. . . . 5
β’ (πΏ β LMod β (πΏ β Grp β§ πΊ β Ring β§ βπ β (BaseβπΊ)βπ β (BaseβπΊ)βπ§ β (BaseβπΏ)βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
43 | 42 | simp2bi 1146 |
. . . 4
β’ (πΏ β LMod β πΊ β Ring) |
44 | | lmodprop2d.p2 |
. . . . 5
β’ (π β π = (BaseβπΊ)) |
45 | | lmodprop2d.2 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΉ)π¦) = (π₯(+gβπΊ)π¦)) |
46 | | lmodprop2d.3 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(.rβπΉ)π¦) = (π₯(.rβπΊ)π¦)) |
47 | 16, 44, 45, 46 | ringpropd 20095 |
. . . 4
β’ (π β (πΉ β Ring β πΊ β Ring)) |
48 | 43, 47 | imbitrrid 245 |
. . 3
β’ (π β (πΏ β LMod β πΉ β Ring)) |
49 | | simplr 767 |
. . . . . . 7
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β πΏ β LMod) |
50 | | simprl 769 |
. . . . . . . 8
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π₯ β π) |
51 | 44 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π = (BaseβπΊ)) |
52 | 50, 51 | eleqtrd 2835 |
. . . . . . 7
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π₯ β (BaseβπΊ)) |
53 | | simprr 771 |
. . . . . . . 8
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π¦ β π΅) |
54 | 30 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π΅ = (BaseβπΏ)) |
55 | 53, 54 | eleqtrd 2835 |
. . . . . . 7
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β π¦ β (BaseβπΏ)) |
56 | 34, 37, 36, 38 | lmodvscl 20481 |
. . . . . . 7
β’ ((πΏ β LMod β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΏ)) β (π₯( Β·π
βπΏ)π¦) β (BaseβπΏ)) |
57 | 49, 52, 55, 56 | syl3anc 1371 |
. . . . . 6
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΏ)π¦) β (BaseβπΏ)) |
58 | | lmodprop2d.4 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
59 | 58 | adantlr 713 |
. . . . . 6
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
60 | 57, 59, 54 | 3eltr4d 2848 |
. . . . 5
β’ (((π β§ πΏ β LMod) β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β π΅) |
61 | 60 | ralrimivva 3200 |
. . . 4
β’ ((π β§ πΏ β LMod) β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) |
62 | 61 | ex 413 |
. . 3
β’ (π β (πΏ β LMod β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) |
63 | 33, 48, 62 | 3jcad 1129 |
. 2
β’ (π β (πΏ β LMod β (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅))) |
64 | 32 | adantr 481 |
. . . . 5
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (πΎ β Grp β πΏ β Grp)) |
65 | 47 | adantr 481 |
. . . . 5
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (πΉ β Ring β πΊ β Ring)) |
66 | | simpll 765 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π) |
67 | | simprlr 778 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π β π) |
68 | | simprrr 780 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π€ β π΅) |
69 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π€ β π΅)) β (π( Β·π
βπΎ)π€) = (π( Β·π
βπΏ)π€)) |
70 | 66, 67, 68, 69 | syl12anc 835 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)π€) = (π( Β·π
βπΏ)π€)) |
71 | 70 | eleq1d 2818 |
. . . . . . . . . . 11
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€) β π΅ β (π( Β·π
βπΏ)π€) β π΅)) |
72 | | simplr1 1215 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β πΎ β Grp) |
73 | 20 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π΅ = (BaseβπΎ)) |
74 | 68, 73 | eleqtrd 2835 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π€ β (BaseβπΎ)) |
75 | | simprrl 779 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π§ β π΅) |
76 | 75, 73 | eleqtrd 2835 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π§ β (BaseβπΎ)) |
77 | 3, 4 | grpcl 18823 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Grp β§ π€ β (BaseβπΎ) β§ π§ β (BaseβπΎ)) β (π€(+gβπΎ)π§) β (BaseβπΎ)) |
78 | 72, 74, 76, 77 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π€(+gβπΎ)π§) β (BaseβπΎ)) |
79 | 78, 73 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π€(+gβπΎ)π§) β π΅) |
80 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ (π€(+gβπΎ)π§) β π΅)) β (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = (π( Β·π
βπΏ)(π€(+gβπΎ)π§))) |
81 | 66, 67, 79, 80 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = (π( Β·π
βπΏ)(π€(+gβπΎ)π§))) |
82 | 31 | oveqrspc2v 7432 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π€ β π΅ β§ π§ β π΅)) β (π€(+gβπΎ)π§) = (π€(+gβπΏ)π§)) |
83 | 66, 68, 75, 82 | syl12anc 835 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π€(+gβπΎ)π§) = (π€(+gβπΏ)π§)) |
84 | 83 | oveq2d 7421 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΏ)(π€(+gβπΎ)π§)) = (π( Β·π
βπΏ)(π€(+gβπΏ)π§))) |
85 | 81, 84 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = (π( Β·π
βπΏ)(π€(+gβπΏ)π§))) |
86 | | simplr3 1217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) |
87 | | ovrspc2v 7431 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π€ β π΅) β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) β (π( Β·π
βπΎ)π€) β π΅) |
88 | 67, 68, 86, 87 | syl21anc 836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)π€) β π΅) |
89 | | ovrspc2v 7431 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π§ β π΅) β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) β (π( Β·π
βπΎ)π§) β π΅) |
90 | 67, 75, 86, 89 | syl21anc 836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)π§) β π΅) |
91 | 31 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)π§) β π΅)) β ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΏ)(π( Β·π
βπΎ)π§))) |
92 | 66, 88, 90, 91 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΏ)(π( Β·π
βπΎ)π§))) |
93 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π§ β π΅)) β (π( Β·π
βπΎ)π§) = (π( Β·π
βπΏ)π§)) |
94 | 66, 67, 75, 93 | syl12anc 835 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)π§) = (π( Β·π
βπΏ)π§)) |
95 | 70, 94 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€)(+gβπΏ)(π( Β·π
βπΎ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§))) |
96 | 92, 95 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§))) |
97 | 85, 96 | eqeq12d 2748 |
. . . . . . . . . . 11
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)))) |
98 | | simplr2 1216 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β πΉ β Ring) |
99 | | simprll 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π β π) |
100 | 16 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π = (BaseβπΉ)) |
101 | 99, 100 | eleqtrd 2835 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π β (BaseβπΉ)) |
102 | 67, 100 | eleqtrd 2835 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β π β (BaseβπΉ)) |
103 | 7, 8 | ringacl 20088 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β Ring β§ π β (BaseβπΉ) β§ π β (BaseβπΉ)) β (π(+gβπΉ)π) β (BaseβπΉ)) |
104 | 98, 101, 102, 103 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π(+gβπΉ)π) β (BaseβπΉ)) |
105 | 104, 100 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π(+gβπΉ)π) β π) |
106 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π(+gβπΉ)π) β π β§ π€ β π΅)) β ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π(+gβπΉ)π)( Β·π
βπΏ)π€)) |
107 | 66, 105, 68, 106 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π(+gβπΉ)π)( Β·π
βπΏ)π€)) |
108 | 45 | oveqrspc2v 7432 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π β π)) β (π(+gβπΉ)π) = (π(+gβπΊ)π)) |
109 | 108 | ad2ant2r 745 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π(+gβπΉ)π) = (π(+gβπΊ)π)) |
110 | 109 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π(+gβπΉ)π)( Β·π
βπΏ)π€) = ((π(+gβπΊ)π)( Β·π
βπΏ)π€)) |
111 | 107, 110 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π(+gβπΊ)π)( Β·π
βπΏ)π€)) |
112 | | ovrspc2v 7431 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π€ β π΅) β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) β (π( Β·π
βπΎ)π€) β π΅) |
113 | 99, 68, 86, 112 | syl21anc 836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)π€) β π΅) |
114 | 31 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)π€) β π΅)) β ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€)) = ((π( Β·π
βπΎ)π€)(+gβπΏ)(π( Β·π
βπΎ)π€))) |
115 | 66, 113, 88, 114 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€)) = ((π( Β·π
βπΎ)π€)(+gβπΏ)(π( Β·π
βπΎ)π€))) |
116 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π€ β π΅)) β (π( Β·π
βπΎ)π€) = (π( Β·π
βπΏ)π€)) |
117 | 66, 99, 68, 116 | syl12anc 835 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)π€) = (π( Β·π
βπΏ)π€)) |
118 | 117, 70 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€)(+gβπΏ)(π( Β·π
βπΎ)π€)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) |
119 | 115, 118 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) |
120 | 111, 119 | eqeq12d 2748 |
. . . . . . . . . . 11
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€)) β ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€)))) |
121 | 71, 97, 120 | 3anbi123d 1436 |
. . . . . . . . . 10
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β ((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))))) |
122 | 7, 9 | ringcl 20066 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β Ring β§ π β (BaseβπΉ) β§ π β (BaseβπΉ)) β (π(.rβπΉ)π) β (BaseβπΉ)) |
123 | 98, 101, 102, 122 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π(.rβπΉ)π) β (BaseβπΉ)) |
124 | 123, 100 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π(.rβπΉ)π) β π) |
125 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π(.rβπΉ)π) β π β§ π€ β π΅)) β ((π(.rβπΉ)π)( Β·π
βπΎ)π€) = ((π(.rβπΉ)π)( Β·π
βπΏ)π€)) |
126 | 66, 124, 68, 125 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π(.rβπΉ)π)( Β·π
βπΎ)π€) = ((π(.rβπΉ)π)( Β·π
βπΏ)π€)) |
127 | 46 | oveqrspc2v 7432 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π β π)) β (π(.rβπΉ)π) = (π(.rβπΊ)π)) |
128 | 127 | ad2ant2r 745 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π(.rβπΉ)π) = (π(.rβπΊ)π)) |
129 | 128 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π(.rβπΉ)π)( Β·π
βπΏ)π€) = ((π(.rβπΊ)π)( Β·π
βπΏ)π€)) |
130 | 126, 129 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((π(.rβπΉ)π)( Β·π
βπΎ)π€) = ((π(.rβπΊ)π)( Β·π
βπΏ)π€)) |
131 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ (π( Β·π
βπΎ)π€) β π΅)) β (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) = (π( Β·π
βπΏ)(π(
Β·π βπΎ)π€))) |
132 | 66, 99, 88, 131 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) = (π( Β·π
βπΏ)(π(
Β·π βπΎ)π€))) |
133 | 70 | oveq2d 7421 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΏ)(π(
Β·π βπΎ)π€)) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€))) |
134 | 132, 133 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€))) |
135 | 130, 134 | eqeq12d 2748 |
. . . . . . . . . . 11
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β ((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)))) |
136 | 7, 10 | ringidcl 20076 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β Ring β
(1rβπΉ)
β (BaseβπΉ)) |
137 | 98, 136 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (1rβπΉ) β (BaseβπΉ)) |
138 | 137, 100 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (1rβπΉ) β π) |
139 | 58 | oveqrspc2v 7432 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((1rβπΉ) β π β§ π€ β π΅)) β ((1rβπΉ)(
Β·π βπΎ)π€) = ((1rβπΉ)( Β·π
βπΏ)π€)) |
140 | 66, 138, 68, 139 | syl12anc 835 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((1rβπΉ)(
Β·π βπΎ)π€) = ((1rβπΉ)( Β·π
βπΏ)π€)) |
141 | 16, 44, 46 | rngidpropd 20221 |
. . . . . . . . . . . . . . 15
β’ (π β (1rβπΉ) = (1rβπΊ)) |
142 | 141 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (1rβπΉ) = (1rβπΊ)) |
143 | 142 | oveq1d 7420 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((1rβπΉ)(
Β·π βπΏ)π€) = ((1rβπΊ)( Β·π
βπΏ)π€)) |
144 | 140, 143 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((1rβπΉ)(
Β·π βπΎ)π€) = ((1rβπΊ)( Β·π
βπΏ)π€)) |
145 | 144 | eqeq1d 2734 |
. . . . . . . . . . 11
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β (((1rβπΉ)(
Β·π βπΎ)π€) = π€ β ((1rβπΊ)(
Β·π βπΏ)π€) = π€)) |
146 | 135, 145 | anbi12d 631 |
. . . . . . . . . 10
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€) β (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€))) |
147 | 121, 146 | anbi12d 631 |
. . . . . . . . 9
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ ((π β π β§ π β π) β§ (π§ β π΅ β§ π€ β π΅))) β ((((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
148 | 147 | anassrs 468 |
. . . . . . . 8
β’ ((((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ (π β π β§ π β π)) β§ (π§ β π΅ β§ π€ β π΅)) β ((((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
149 | 148 | 2ralbidva 3216 |
. . . . . . 7
β’ (((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β§ (π β π β§ π β π)) β (βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
150 | 149 | 2ralbidva 3216 |
. . . . . 6
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ β π βπ β π βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ β π βπ β π βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
151 | 16 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β π = (BaseβπΉ)) |
152 | 20 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β π΅ = (BaseβπΎ)) |
153 | 152 | eleq2d 2819 |
. . . . . . . . . . . 12
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β ((π( Β·π
βπΎ)π€) β π΅ β (π( Β·π
βπΎ)π€) β (BaseβπΎ))) |
154 | 153 | 3anbi1d 1440 |
. . . . . . . . . . 11
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β ((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))))) |
155 | 154 | anbi1d 630 |
. . . . . . . . . 10
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β ((((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β (((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)))) |
156 | 152, 155 | raleqbidv 3342 |
. . . . . . . . 9
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ€ β π΅ (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)))) |
157 | 152, 156 | raleqbidv 3342 |
. . . . . . . 8
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ§ β (BaseβπΎ)βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)))) |
158 | 151, 157 | raleqbidv 3342 |
. . . . . . 7
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ β π βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ β (BaseβπΉ)βπ§ β (BaseβπΎ)βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)))) |
159 | 151, 158 | raleqbidv 3342 |
. . . . . 6
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ β π βπ β π βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΎ)π€) β π΅ β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ β (BaseβπΉ)βπ β (BaseβπΉ)βπ§ β (BaseβπΎ)βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)))) |
160 | 44 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β π = (BaseβπΊ)) |
161 | 30 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β π΅ = (BaseβπΏ)) |
162 | 161 | eleq2d 2819 |
. . . . . . . . . . . 12
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β ((π( Β·π
βπΏ)π€) β π΅ β (π( Β·π
βπΏ)π€) β (BaseβπΏ))) |
163 | 162 | 3anbi1d 1440 |
. . . . . . . . . . 11
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β ((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))))) |
164 | 163 | anbi1d 630 |
. . . . . . . . . 10
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β ((((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)) β (((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
165 | 161, 164 | raleqbidv 3342 |
. . . . . . . . 9
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ€ β π΅ (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)) β βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
166 | 161, 165 | raleqbidv 3342 |
. . . . . . . 8
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)) β βπ§ β (BaseβπΏ)βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
167 | 160, 166 | raleqbidv 3342 |
. . . . . . 7
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ β π βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)) β βπ β (BaseβπΊ)βπ§ β (BaseβπΏ)βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
168 | 160, 167 | raleqbidv 3342 |
. . . . . 6
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ β π βπ β π βπ§ β π΅ βπ€ β π΅ (((π( Β·π
βπΏ)π€) β π΅ β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)) β βπ β (BaseβπΊ)βπ β (BaseβπΊ)βπ§ β (BaseβπΏ)βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
169 | 150, 159,
168 | 3bitr3d 308 |
. . . . 5
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (βπ β (BaseβπΉ)βπ β (BaseβπΉ)βπ§ β (BaseβπΎ)βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€)) β βπ β (BaseβπΊ)βπ β (BaseβπΊ)βπ§ β (BaseβπΏ)βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€)))) |
170 | 64, 65, 169 | 3anbi123d 1436 |
. . . 4
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β ((πΎ β Grp β§ πΉ β Ring β§ βπ β (BaseβπΉ)βπ β (BaseβπΉ)βπ§ β (BaseβπΎ)βπ€ β (BaseβπΎ)(((π( Β·π
βπΎ)π€) β (BaseβπΎ) β§ (π( Β·π
βπΎ)(π€(+gβπΎ)π§)) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π§)) β§ ((π(+gβπΉ)π)( Β·π
βπΎ)π€) = ((π( Β·π
βπΎ)π€)(+gβπΎ)(π( Β·π
βπΎ)π€))) β§ (((π(.rβπΉ)π)( Β·π
βπΎ)π€) = (π( Β·π
βπΎ)(π(
Β·π βπΎ)π€)) β§ ((1rβπΉ)(
Β·π βπΎ)π€) = π€))) β (πΏ β Grp β§ πΊ β Ring β§ βπ β (BaseβπΊ)βπ β (BaseβπΊ)βπ§ β (BaseβπΏ)βπ€ β (BaseβπΏ)(((π( Β·π
βπΏ)π€) β (BaseβπΏ) β§ (π( Β·π
βπΏ)(π€(+gβπΏ)π§)) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π§)) β§ ((π(+gβπΊ)π)( Β·π
βπΏ)π€) = ((π( Β·π
βπΏ)π€)(+gβπΏ)(π( Β·π
βπΏ)π€))) β§ (((π(.rβπΊ)π)( Β·π
βπΏ)π€) = (π( Β·π
βπΏ)(π(
Β·π βπΏ)π€)) β§ ((1rβπΊ)(
Β·π βπΏ)π€) = π€))))) |
171 | 170, 11, 42 | 3bitr4g 313 |
. . 3
β’ ((π β§ (πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅)) β (πΎ β LMod β πΏ β LMod)) |
172 | 171 | ex 413 |
. 2
β’ (π β ((πΎ β Grp β§ πΉ β Ring β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π΅) β (πΎ β LMod β πΏ β LMod))) |
173 | 28, 63, 172 | pm5.21ndd 380 |
1
β’ (π β (πΎ β LMod β πΏ β LMod)) |