Step | Hyp | Ref
| Expression |
1 | | quslsm.n |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
2 | | subgrcl 18805 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | quslsm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
5 | 4 | subgss 18801 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) |
6 | 1, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
7 | | eqid 2736 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
8 | | eqid 2736 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
9 | | eqid 2736 |
. . . . . 6
⊢ (𝐺 ~QG 𝑆) = (𝐺 ~QG 𝑆) |
10 | 4, 7, 8, 9 | eqgfval 18849 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝐺 ~QG 𝑆) = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆)}) |
11 | 3, 6, 10 | syl2anc 585 |
. . . 4
⊢ (𝜑 → (𝐺 ~QG 𝑆) = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆)}) |
12 | | simpr 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) |
13 | | oveq2 7315 |
. . . . . . . . . 10
⊢ (𝑘 =
(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) → (𝑖(+g‘𝐺)𝑘) = (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗))) |
14 | 13 | eqeq1d 2738 |
. . . . . . . . 9
⊢ (𝑘 =
(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) → ((𝑖(+g‘𝐺)𝑘) = 𝑗 ↔ (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) = 𝑗)) |
15 | 14 | adantl 483 |
. . . . . . . 8
⊢ ((((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) ∧ 𝑘 = (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) → ((𝑖(+g‘𝐺)𝑘) = 𝑗 ↔ (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) = 𝑗)) |
16 | 3 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → 𝐺 ∈ Grp) |
17 | | vex 3441 |
. . . . . . . . . . . . . . . 16
⊢ 𝑖 ∈ V |
18 | | vex 3441 |
. . . . . . . . . . . . . . . 16
⊢ 𝑗 ∈ V |
19 | 17, 18 | prss 4759 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) ↔ {𝑖, 𝑗} ⊆ 𝐵) |
20 | 19 | bicomi 223 |
. . . . . . . . . . . . . 14
⊢ ({𝑖, 𝑗} ⊆ 𝐵 ↔ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) |
21 | 20 | simplbi 499 |
. . . . . . . . . . . . 13
⊢ ({𝑖, 𝑗} ⊆ 𝐵 → 𝑖 ∈ 𝐵) |
22 | 21 | adantl 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → 𝑖 ∈ 𝐵) |
23 | | eqid 2736 |
. . . . . . . . . . . . 13
⊢
(0g‘𝐺) = (0g‘𝐺) |
24 | 4, 8, 23, 7 | grprinv 18674 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝐵) → (𝑖(+g‘𝐺)((invg‘𝐺)‘𝑖)) = (0g‘𝐺)) |
25 | 16, 22, 24 | syl2anc 585 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → (𝑖(+g‘𝐺)((invg‘𝐺)‘𝑖)) = (0g‘𝐺)) |
26 | 25 | oveq1d 7322 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → ((𝑖(+g‘𝐺)((invg‘𝐺)‘𝑖))(+g‘𝐺)𝑗) = ((0g‘𝐺)(+g‘𝐺)𝑗)) |
27 | 4, 7 | grpinvcl 18672 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝐵) → ((invg‘𝐺)‘𝑖) ∈ 𝐵) |
28 | 16, 22, 27 | syl2anc 585 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → ((invg‘𝐺)‘𝑖) ∈ 𝐵) |
29 | 20 | simprbi 498 |
. . . . . . . . . . . 12
⊢ ({𝑖, 𝑗} ⊆ 𝐵 → 𝑗 ∈ 𝐵) |
30 | 29 | adantl 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → 𝑗 ∈ 𝐵) |
31 | 4, 8 | grpass 18631 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑖 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑖) ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → ((𝑖(+g‘𝐺)((invg‘𝐺)‘𝑖))(+g‘𝐺)𝑗) = (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗))) |
32 | 16, 22, 28, 30, 31 | syl13anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → ((𝑖(+g‘𝐺)((invg‘𝐺)‘𝑖))(+g‘𝐺)𝑗) = (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗))) |
33 | 4, 8, 23 | grplid 18654 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑗 ∈ 𝐵) → ((0g‘𝐺)(+g‘𝐺)𝑗) = 𝑗) |
34 | 16, 30, 33 | syl2anc 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → ((0g‘𝐺)(+g‘𝐺)𝑗) = 𝑗) |
35 | 26, 32, 34 | 3eqtr3d 2784 |
. . . . . . . . 9
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) = 𝑗) |
36 | 35 | adantr 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) → (𝑖(+g‘𝐺)(((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) = 𝑗) |
37 | 12, 15, 36 | rspcedvd 3568 |
. . . . . . 7
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) → ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗) |
38 | | oveq2 7315 |
. . . . . . . . . . 11
⊢ ((𝑖(+g‘𝐺)𝑘) = 𝑗 → (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘)) = (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) |
39 | 38 | adantl 483 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) ∧ (𝑖(+g‘𝐺)𝑘) = 𝑗) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘)) = (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗)) |
40 | | simpll 765 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) → 𝜑) |
41 | 22 | adantr 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) → 𝑖 ∈ 𝐵) |
42 | 6 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → 𝑆 ⊆ 𝐵) |
43 | 42 | sselda 3926 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝐵) |
44 | 3 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → 𝐺 ∈ Grp) |
45 | | simp2 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → 𝑖 ∈ 𝐵) |
46 | 4, 8, 23, 7 | grplinv 18673 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝑖 ∈ 𝐵) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑖) = (0g‘𝐺)) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑖) = (0g‘𝐺)) |
48 | 47 | oveq1d 7322 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → ((((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑖)(+g‘𝐺)𝑘) = ((0g‘𝐺)(+g‘𝐺)𝑘)) |
49 | 44, 45, 27 | syl2anc 585 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → ((invg‘𝐺)‘𝑖) ∈ 𝐵) |
50 | | simp3 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵) |
51 | 4, 8 | grpass 18631 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑖) ∈ 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵)) → ((((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑖)(+g‘𝐺)𝑘) = (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘))) |
52 | 44, 49, 45, 50, 51 | syl13anc 1372 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → ((((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑖)(+g‘𝐺)𝑘) = (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘))) |
53 | 4, 8, 23 | grplid 18654 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑘 ∈ 𝐵) → ((0g‘𝐺)(+g‘𝐺)𝑘) = 𝑘) |
54 | 44, 50, 53 | syl2anc 585 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → ((0g‘𝐺)(+g‘𝐺)𝑘) = 𝑘) |
55 | 48, 52, 54 | 3eqtr3d 2784 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘)) = 𝑘) |
56 | 40, 41, 43, 55 | syl3anc 1371 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘)) = 𝑘) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) ∧ (𝑖(+g‘𝐺)𝑘) = 𝑗) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)(𝑖(+g‘𝐺)𝑘)) = 𝑘) |
58 | 39, 57 | eqtr3d 2778 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) ∧ (𝑖(+g‘𝐺)𝑘) = 𝑗) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) = 𝑘) |
59 | | simplr 767 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) ∧ (𝑖(+g‘𝐺)𝑘) = 𝑗) → 𝑘 ∈ 𝑆) |
60 | 58, 59 | eqeltrd 2837 |
. . . . . . . 8
⊢ ((((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ 𝑘 ∈ 𝑆) ∧ (𝑖(+g‘𝐺)𝑘) = 𝑗) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) |
61 | 60 | r19.29an 3152 |
. . . . . . 7
⊢ (((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗) → (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) |
62 | 37, 61 | impbida 799 |
. . . . . 6
⊢ ((𝜑 ∧ {𝑖, 𝑗} ⊆ 𝐵) → ((((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆 ↔ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)) |
63 | 62 | pm5.32da 580 |
. . . . 5
⊢ (𝜑 → (({𝑖, 𝑗} ⊆ 𝐵 ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆) ↔ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗))) |
64 | 63 | opabbidv 5147 |
. . . 4
⊢ (𝜑 → {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ (((invg‘𝐺)‘𝑖)(+g‘𝐺)𝑗) ∈ 𝑆)} = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)}) |
65 | 11, 64 | eqtrd 2776 |
. . 3
⊢ (𝜑 → (𝐺 ~QG 𝑆) = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)}) |
66 | 65 | eceq2d 8571 |
. 2
⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑆) = [𝑋]{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)}) |
67 | | quslsm.p |
. . 3
⊢ ⊕ =
(LSSum‘𝐺) |
68 | | eqid 2736 |
. . 3
⊢
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)} = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)} |
69 | 3 | grpmndd 18634 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
70 | | quslsm.s |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
71 | 4, 8, 67, 68, 69, 6, 70 | lsmsnorb2 31625 |
. 2
⊢ (𝜑 → ({𝑋} ⊕ 𝑆) = [𝑋]{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ ∃𝑘 ∈ 𝑆 (𝑖(+g‘𝐺)𝑘) = 𝑗)}) |
72 | 66, 71 | eqtr4d 2779 |
1
⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑆) = ({𝑋} ⊕ 𝑆)) |