Step | Hyp | Ref
| Expression |
1 | | lmodgrp 19906 |
. . . 4
⊢ (𝐾 ∈ LMod → 𝐾 ∈ Grp) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐾 ∈ LMod → 𝐾 ∈ Grp)) |
3 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
4 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐾) = (+g‘𝐾) |
5 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝐾) = ( ·𝑠
‘𝐾) |
6 | | lmodprop2d.f |
. . . . . 6
⊢ 𝐹 = (Scalar‘𝐾) |
7 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐹) =
(Base‘𝐹) |
8 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐹) = (+g‘𝐹) |
9 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝐹) = (.r‘𝐹) |
10 | | eqid 2737 |
. . . . . 6
⊢
(1r‘𝐹) = (1r‘𝐹) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | islmod 19903 |
. . . . 5
⊢ (𝐾 ∈ LMod ↔ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)(((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)))) |
12 | 11 | simp2bi 1148 |
. . . 4
⊢ (𝐾 ∈ LMod → 𝐹 ∈ Ring) |
13 | 12 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐾 ∈ LMod → 𝐹 ∈ Ring)) |
14 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝐾 ∈ LMod) |
15 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝑃) |
16 | | lmodprop2d.p1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 = (Base‘𝐹)) |
17 | 16 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑃 = (Base‘𝐹)) |
18 | 15, 17 | eleqtrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (Base‘𝐹)) |
19 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
20 | | lmodprop2d.b1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
21 | 20 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝐵 = (Base‘𝐾)) |
22 | 19, 21 | eleqtrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘𝐾)) |
23 | 3, 6, 5, 7 | lmodvscl 19916 |
. . . . . . 7
⊢ ((𝐾 ∈ LMod ∧ 𝑥 ∈ (Base‘𝐹) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑥( ·𝑠
‘𝐾)𝑦) ∈ (Base‘𝐾)) |
24 | 14, 18, 22, 23 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) ∈ (Base‘𝐾)) |
25 | 24, 21 | eleqtrrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ 𝐾 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) |
26 | 25 | ralrimivva 3112 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ LMod) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) |
27 | 26 | ex 416 |
. . 3
⊢ (𝜑 → (𝐾 ∈ LMod → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) |
28 | 2, 13, 27 | 3jcad 1131 |
. 2
⊢ (𝜑 → (𝐾 ∈ LMod → (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵))) |
29 | | lmodgrp 19906 |
. . . 4
⊢ (𝐿 ∈ LMod → 𝐿 ∈ Grp) |
30 | | lmodprop2d.b2 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
31 | | lmodprop2d.1 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) |
32 | 20, 30, 31 | grppropd 18382 |
. . . 4
⊢ (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)) |
33 | 29, 32 | syl5ibr 249 |
. . 3
⊢ (𝜑 → (𝐿 ∈ LMod → 𝐾 ∈ Grp)) |
34 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐿) =
(Base‘𝐿) |
35 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐿) = (+g‘𝐿) |
36 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝐿) = ( ·𝑠
‘𝐿) |
37 | | lmodprop2d.g |
. . . . . 6
⊢ 𝐺 = (Scalar‘𝐿) |
38 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
39 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
40 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝐺) = (.r‘𝐺) |
41 | | eqid 2737 |
. . . . . 6
⊢
(1r‘𝐺) = (1r‘𝐺) |
42 | 34, 35, 36, 37, 38, 39, 40, 41 | islmod 19903 |
. . . . 5
⊢ (𝐿 ∈ LMod ↔ (𝐿 ∈ Grp ∧ 𝐺 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐺)∀𝑟 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)(((𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿) ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
43 | 42 | simp2bi 1148 |
. . . 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 19600 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ Ring ↔ 𝐺 ∈ Ring)) |
48 | 43, 47 | syl5ibr 249 |
. . 3
⊢ (𝜑 → (𝐿 ∈ LMod → 𝐹 ∈ Ring)) |
49 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝐿 ∈ LMod) |
50 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝑃) |
51 | 44 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑃 = (Base‘𝐺)) |
52 | 50, 51 | eleqtrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (Base‘𝐺)) |
53 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
54 | 30 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝐵 = (Base‘𝐿)) |
55 | 53, 54 | eleqtrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘𝐿)) |
56 | 34, 37, 36, 38 | lmodvscl 19916 |
. . . . . . 7
⊢ ((𝐿 ∈ LMod ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐿)) → (𝑥( ·𝑠
‘𝐿)𝑦) ∈ (Base‘𝐿)) |
57 | 49, 52, 55, 56 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐿)𝑦) ∈ (Base‘𝐿)) |
58 | | lmodprop2d.4 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) = (𝑥( ·𝑠
‘𝐿)𝑦)) |
59 | 58 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) = (𝑥( ·𝑠
‘𝐿)𝑦)) |
60 | 57, 59, 54 | 3eltr4d 2853 |
. . . . 5
⊢ (((𝜑 ∧ 𝐿 ∈ LMod) ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) |
61 | 60 | ralrimivva 3112 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 ∈ LMod) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) |
62 | 61 | ex 416 |
. . 3
⊢ (𝜑 → (𝐿 ∈ LMod → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) |
63 | 33, 48, 62 | 3jcad 1131 |
. 2
⊢ (𝜑 → (𝐿 ∈ LMod → (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵))) |
64 | 32 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)) |
65 | 47 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (𝐹 ∈ Ring ↔ 𝐺 ∈ Ring)) |
66 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝜑) |
67 | | simprlr 780 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑟 ∈ 𝑃) |
68 | | simprrr 782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑤 ∈ 𝐵) |
69 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵)) → (𝑟( ·𝑠
‘𝐾)𝑤) = (𝑟( ·𝑠
‘𝐿)𝑤)) |
70 | 66, 67, 68, 69 | syl12anc 837 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐾)𝑤) = (𝑟( ·𝑠
‘𝐿)𝑤)) |
71 | 70 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ↔ (𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵)) |
72 | | simplr1 1217 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝐾 ∈ Grp) |
73 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝐵 = (Base‘𝐾)) |
74 | 68, 73 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑤 ∈ (Base‘𝐾)) |
75 | | simprrl 781 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑧 ∈ 𝐵) |
76 | 75, 73 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑧 ∈ (Base‘𝐾)) |
77 | 3, 4 | grpcl 18373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Grp ∧ 𝑤 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑤(+g‘𝐾)𝑧) ∈ (Base‘𝐾)) |
78 | 72, 74, 76, 77 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑤(+g‘𝐾)𝑧) ∈ (Base‘𝐾)) |
79 | 78, 73 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑤(+g‘𝐾)𝑧) ∈ 𝐵) |
80 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑃 ∧ (𝑤(+g‘𝐾)𝑧) ∈ 𝐵)) → (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐾)𝑧))) |
81 | 66, 67, 79, 80 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐾)𝑧))) |
82 | 31 | oveqrspc2v 7240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑤(+g‘𝐾)𝑧) = (𝑤(+g‘𝐿)𝑧)) |
83 | 66, 68, 75, 82 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑤(+g‘𝐾)𝑧) = (𝑤(+g‘𝐿)𝑧)) |
84 | 83 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐾)𝑧)) = (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧))) |
85 | 81, 84 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧))) |
86 | | simplr3 1219 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) |
87 | | ovrspc2v 7239 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) → (𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵) |
88 | 67, 68, 86, 87 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵) |
89 | | ovrspc2v 7239 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) → (𝑟( ·𝑠
‘𝐾)𝑧) ∈ 𝐵) |
90 | 67, 75, 86, 89 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐾)𝑧) ∈ 𝐵) |
91 | 31 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)𝑧) ∈ 𝐵)) → ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐾)𝑧))) |
92 | 66, 88, 90, 91 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐾)𝑧))) |
93 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵)) → (𝑟( ·𝑠
‘𝐾)𝑧) = (𝑟( ·𝑠
‘𝐿)𝑧)) |
94 | 66, 67, 75, 93 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑟( ·𝑠
‘𝐾)𝑧) = (𝑟( ·𝑠
‘𝐿)𝑧)) |
95 | 70, 94 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧))) |
96 | 92, 95 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧))) |
97 | 85, 96 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ↔ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)))) |
98 | | simplr2 1218 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝐹 ∈ Ring) |
99 | | simprll 779 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑞 ∈ 𝑃) |
100 | 16 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑃 = (Base‘𝐹)) |
101 | 99, 100 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑞 ∈ (Base‘𝐹)) |
102 | 67, 100 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → 𝑟 ∈ (Base‘𝐹)) |
103 | 7, 8 | ringacl 19596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Ring ∧ 𝑞 ∈ (Base‘𝐹) ∧ 𝑟 ∈ (Base‘𝐹)) → (𝑞(+g‘𝐹)𝑟) ∈ (Base‘𝐹)) |
104 | 98, 101, 102, 103 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞(+g‘𝐹)𝑟) ∈ (Base‘𝐹)) |
105 | 104, 100 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞(+g‘𝐹)𝑟) ∈ 𝑃) |
106 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑞(+g‘𝐹)𝑟) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵)) → ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐿)𝑤)) |
107 | 66, 105, 68, 106 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐿)𝑤)) |
108 | 45 | oveqrspc2v 7240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃)) → (𝑞(+g‘𝐹)𝑟) = (𝑞(+g‘𝐺)𝑟)) |
109 | 108 | ad2ant2r 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞(+g‘𝐹)𝑟) = (𝑞(+g‘𝐺)𝑟)) |
110 | 109 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤)) |
111 | 107, 110 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤)) |
112 | | ovrspc2v 7239 |
. . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) → (𝑞( ·𝑠
‘𝐾)𝑤) ∈ 𝐵) |
113 | 99, 68, 86, 112 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞( ·𝑠
‘𝐾)𝑤) ∈ 𝐵) |
114 | 31 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑞( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵)) → ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤)) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐾)𝑤))) |
115 | 66, 113, 88, 114 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤)) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐾)𝑤))) |
116 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵)) → (𝑞( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐿)𝑤)) |
117 | 66, 99, 68, 116 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐿)𝑤)) |
118 | 117, 70 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐾)𝑤)) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) |
119 | 115, 118 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤)) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) |
120 | 111, 119 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤)) ↔ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤)))) |
121 | 71, 97, 120 | 3anbi123d 1438 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ↔ ((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))))) |
122 | 7, 9 | ringcl 19579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Ring ∧ 𝑞 ∈ (Base‘𝐹) ∧ 𝑟 ∈ (Base‘𝐹)) → (𝑞(.r‘𝐹)𝑟) ∈ (Base‘𝐹)) |
123 | 98, 101, 102, 122 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞(.r‘𝐹)𝑟) ∈ (Base‘𝐹)) |
124 | 123, 100 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞(.r‘𝐹)𝑟) ∈ 𝑃) |
125 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑞(.r‘𝐹)𝑟) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵)) → ((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐿)𝑤)) |
126 | 66, 124, 68, 125 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐿)𝑤)) |
127 | 46 | oveqrspc2v 7240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃)) → (𝑞(.r‘𝐹)𝑟) = (𝑞(.r‘𝐺)𝑟)) |
128 | 127 | ad2ant2r 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞(.r‘𝐹)𝑟) = (𝑞(.r‘𝐺)𝑟)) |
129 | 128 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤)) |
130 | 126, 129 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤)) |
131 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑃 ∧ (𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵)) → (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐾)𝑤))) |
132 | 66, 99, 88, 131 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐾)𝑤))) |
133 | 70 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐾)𝑤)) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤))) |
134 | 132, 133 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤))) |
135 | 130, 134 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ↔ ((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)))) |
136 | 7, 10 | ringidcl 19586 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Ring →
(1r‘𝐹)
∈ (Base‘𝐹)) |
137 | 98, 136 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (1r‘𝐹) ∈ (Base‘𝐹)) |
138 | 137, 100 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (1r‘𝐹) ∈ 𝑃) |
139 | 58 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((1r‘𝐹) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵)) → ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = ((1r‘𝐹)( ·𝑠
‘𝐿)𝑤)) |
140 | 66, 138, 68, 139 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = ((1r‘𝐹)( ·𝑠
‘𝐿)𝑤)) |
141 | 16, 44, 46 | rngidpropd 19713 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1r‘𝐹) = (1r‘𝐺)) |
142 | 141 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (1r‘𝐹) = (1r‘𝐺)) |
143 | 142 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((1r‘𝐹)(
·𝑠 ‘𝐿)𝑤) = ((1r‘𝐺)( ·𝑠
‘𝐿)𝑤)) |
144 | 140, 143 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = ((1r‘𝐺)( ·𝑠
‘𝐿)𝑤)) |
145 | 144 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → (((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤 ↔ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)) |
146 | 135, 145 | anbi12d 634 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤) ↔ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤))) |
147 | 121, 146 | anbi12d 634 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ ((𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) → ((((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
148 | 147 | anassrs 471 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ (𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
149 | 148 | 2ralbidva 3119 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) ∧ (𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃)) → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
150 | 149 | 2ralbidva 3119 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑞 ∈ 𝑃 ∀𝑟 ∈ 𝑃 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ ∀𝑞 ∈ 𝑃 ∀𝑟 ∈ 𝑃 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
151 | 16 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → 𝑃 = (Base‘𝐹)) |
152 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → 𝐵 = (Base‘𝐾)) |
153 | 152 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → ((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ↔ (𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾))) |
154 | 153 | 3anbi1d 1442 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ↔ ((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))))) |
155 | 154 | anbi1d 633 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → ((((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)))) |
156 | 152, 155 | raleqbidv 3313 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ ∀𝑤 ∈ (Base‘𝐾)(((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)))) |
157 | 152, 156 | raleqbidv 3313 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ ∀𝑧 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)(((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)))) |
158 | 151, 157 | raleqbidv 3313 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑟 ∈ 𝑃 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ ∀𝑟 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)(((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)))) |
159 | 151, 158 | raleqbidv 3313 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑞 ∈ 𝑃 ∀𝑟 ∈ 𝑃 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)) ↔ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)(((𝑟( ·𝑠
‘𝐾)𝑤) ∈ (Base‘𝐾) ∧ (𝑟( ·𝑠
‘𝐾)(𝑤(+g‘𝐾)𝑧)) = ((𝑟( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑧)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = ((𝑞( ·𝑠
‘𝐾)𝑤)(+g‘𝐾)(𝑟( ·𝑠
‘𝐾)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠
‘𝐾)𝑤) = (𝑞( ·𝑠
‘𝐾)(𝑟(
·𝑠 ‘𝐾)𝑤)) ∧ ((1r‘𝐹)(
·𝑠 ‘𝐾)𝑤) = 𝑤)))) |
160 | 44 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → 𝑃 = (Base‘𝐺)) |
161 | 30 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → 𝐵 = (Base‘𝐿)) |
162 | 161 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → ((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ↔ (𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿))) |
163 | 162 | 3anbi1d 1442 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ↔ ((𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿) ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))))) |
164 | 163 | anbi1d 633 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → ((((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿) ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
165 | 161, 164 | raleqbidv 3313 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)) ↔ ∀𝑤 ∈ (Base‘𝐿)(((𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿) ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
166 | 161, 165 | raleqbidv 3313 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)) ↔ ∀𝑧 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)(((𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿) ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
167 | 160, 166 | raleqbidv 3313 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (∀𝑟 ∈ 𝑃 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (((𝑟( ·𝑠
‘𝐿)𝑤) ∈ 𝐵 ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)) ↔ ∀𝑟 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)(((𝑟( ·𝑠
‘𝐿)𝑤) ∈ (Base‘𝐿) ∧ (𝑟( ·𝑠
‘𝐿)(𝑤(+g‘𝐿)𝑧)) = ((𝑟( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑧)) ∧ ((𝑞(+g‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = ((𝑞( ·𝑠
‘𝐿)𝑤)(+g‘𝐿)(𝑟( ·𝑠
‘𝐿)𝑤))) ∧ (((𝑞(.r‘𝐺)𝑟)( ·𝑠
‘𝐿)𝑤) = (𝑞( ·𝑠
‘𝐿)(𝑟(
·𝑠 ‘𝐿)𝑤)) ∧ ((1r‘𝐺)(
·𝑠 ‘𝐿)𝑤) = 𝑤)))) |
168 | 160, 167 | raleqbidv 3313 |
. . . . . 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 312 |
. . . . 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 1438 |
. . . 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 317 |
. . 3
⊢ ((𝜑 ∧ (𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵)) → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod)) |
172 | 171 | ex 416 |
. 2
⊢ (𝜑 → ((𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝐵) → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod))) |
173 | 28, 63, 172 | pm5.21ndd 384 |
1
⊢ (𝜑 → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod)) |