Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. 2
⊢ (𝜑 → (𝑃 ↾s 𝐻) = (𝑃 ↾s 𝐻)) |
2 | | eqidd 2611 |
. 2
⊢ (𝜑 → (0g‘𝑃) = (0g‘𝑃)) |
3 | | eqidd 2611 |
. 2
⊢ (𝜑 → (+g‘𝑃) = (+g‘𝑃)) |
4 | | dsmmsubg.r |
. . . . . 6
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
5 | | dsmmsubg.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
6 | | fex 6394 |
. . . . . 6
⊢ ((𝑅:𝐼⟶Grp ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ V) |
7 | 4, 5, 6 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ V) |
8 | | eqid 2610 |
. . . . . 6
⊢ {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} = {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} |
9 | 8 | dsmmbase 19898 |
. . . . 5
⊢ (𝑅 ∈ V → {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} = (Base‘(𝑆 ⊕m 𝑅))) |
10 | 7, 9 | syl 17 |
. . . 4
⊢ (𝜑 → {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} = (Base‘(𝑆 ⊕m 𝑅))) |
11 | | ssrab2 3650 |
. . . 4
⊢ {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} ⊆ (Base‘(𝑆Xs𝑅)) |
12 | 10, 11 | syl6eqssr 3619 |
. . 3
⊢ (𝜑 → (Base‘(𝑆 ⊕m 𝑅)) ⊆ (Base‘(𝑆Xs𝑅))) |
13 | | dsmmsubg.h |
. . 3
⊢ 𝐻 = (Base‘(𝑆 ⊕m 𝑅)) |
14 | | dsmmsubg.p |
. . . 4
⊢ 𝑃 = (𝑆Xs𝑅) |
15 | 14 | fveq2i 6106 |
. . 3
⊢
(Base‘𝑃) =
(Base‘(𝑆Xs𝑅)) |
16 | 12, 13, 15 | 3sstr4g 3609 |
. 2
⊢ (𝜑 → 𝐻 ⊆ (Base‘𝑃)) |
17 | | dsmmsubg.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
18 | | grpmnd 17252 |
. . . . 5
⊢ (𝑎 ∈ Grp → 𝑎 ∈ Mnd) |
19 | 18 | ssriv 3572 |
. . . 4
⊢ Grp
⊆ Mnd |
20 | | fss 5969 |
. . . 4
⊢ ((𝑅:𝐼⟶Grp ∧ Grp ⊆ Mnd) →
𝑅:𝐼⟶Mnd) |
21 | 4, 19, 20 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
22 | | eqid 2610 |
. . 3
⊢
(0g‘𝑃) = (0g‘𝑃) |
23 | 14, 13, 5, 17, 21, 22 | dsmm0cl 19903 |
. 2
⊢ (𝜑 → (0g‘𝑃) ∈ 𝐻) |
24 | 5 | 3ad2ant1 1075 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝐼 ∈ 𝑊) |
25 | 17 | 3ad2ant1 1075 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑆 ∈ 𝑉) |
26 | 21 | 3ad2ant1 1075 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑅:𝐼⟶Mnd) |
27 | | simp2 1055 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑎 ∈ 𝐻) |
28 | | simp3 1056 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑏 ∈ 𝐻) |
29 | | eqid 2610 |
. . 3
⊢
(+g‘𝑃) = (+g‘𝑃) |
30 | 14, 13, 24, 25, 26, 27, 28, 29 | dsmmacl 19904 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → (𝑎(+g‘𝑃)𝑏) ∈ 𝐻) |
31 | 14, 5, 17, 4 | prdsgrpd 17348 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) |
32 | 31 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑃 ∈ Grp) |
33 | 16 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 ∈ (Base‘𝑃)) |
34 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) |
35 | | eqid 2610 |
. . . . 5
⊢
(invg‘𝑃) = (invg‘𝑃) |
36 | 34, 35 | grpinvcl 17290 |
. . . 4
⊢ ((𝑃 ∈ Grp ∧ 𝑎 ∈ (Base‘𝑃)) →
((invg‘𝑃)‘𝑎) ∈ (Base‘𝑃)) |
37 | 32, 33, 36 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((invg‘𝑃)‘𝑎) ∈ (Base‘𝑃)) |
38 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 ∈ 𝐻) |
39 | | eqid 2610 |
. . . . . . 7
⊢ (𝑆 ⊕m 𝑅) = (𝑆 ⊕m 𝑅) |
40 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐼 ∈ 𝑊) |
41 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑅:𝐼⟶Grp → 𝑅 Fn 𝐼) |
42 | 4, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
43 | 42 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑅 Fn 𝐼) |
44 | 14, 39, 34, 13, 40, 43 | dsmmelbas 19902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑎 ∈ 𝐻 ↔ (𝑎 ∈ (Base‘𝑃) ∧ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin))) |
45 | 38, 44 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑎 ∈ (Base‘𝑃) ∧ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin)) |
46 | 45 | simprd 478 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin) |
47 | 5 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
48 | 17 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
49 | 4 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑅:𝐼⟶Grp) |
50 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑃)) |
51 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑏 ∈ 𝐼) |
52 | 14, 47, 48, 49, 34, 35, 50, 51 | prdsinvgd2 19905 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → (((invg‘𝑃)‘𝑎)‘𝑏) = ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏))) |
53 | 52 | adantrr 749 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → (((invg‘𝑃)‘𝑎)‘𝑏) = ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏))) |
54 | | fveq2 6103 |
. . . . . . . . 9
⊢ ((𝑎‘𝑏) = (0g‘(𝑅‘𝑏)) → ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏)) = ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏)))) |
55 | 54 | ad2antll 761 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏)) = ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏)))) |
56 | 4 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐼) → (𝑅‘𝑏) ∈ Grp) |
57 | 56 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → (𝑅‘𝑏) ∈ Grp) |
58 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘(𝑅‘𝑏)) = (0g‘(𝑅‘𝑏)) |
59 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(invg‘(𝑅‘𝑏)) = (invg‘(𝑅‘𝑏)) |
60 | 58, 59 | grpinvid 17299 |
. . . . . . . . . 10
⊢ ((𝑅‘𝑏) ∈ Grp →
((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏))) = (0g‘(𝑅‘𝑏))) |
61 | 57, 60 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏))) = (0g‘(𝑅‘𝑏))) |
62 | 61 | adantrr 749 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏))) = (0g‘(𝑅‘𝑏))) |
63 | 53, 55, 62 | 3eqtrd 2648 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → (((invg‘𝑃)‘𝑎)‘𝑏) = (0g‘(𝑅‘𝑏))) |
64 | 63 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → ((𝑎‘𝑏) = (0g‘(𝑅‘𝑏)) → (((invg‘𝑃)‘𝑎)‘𝑏) = (0g‘(𝑅‘𝑏)))) |
65 | 64 | necon3d 2803 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → ((((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏)) → (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏)))) |
66 | 65 | ss2rabdv 3646 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ⊆ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))}) |
67 | | ssfi 8065 |
. . . 4
⊢ (({𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin ∧ {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ⊆ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))}) → {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin) |
68 | 46, 66, 67 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin) |
69 | 14, 39, 34, 13, 40, 43 | dsmmelbas 19902 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (((invg‘𝑃)‘𝑎) ∈ 𝐻 ↔ (((invg‘𝑃)‘𝑎) ∈ (Base‘𝑃) ∧ {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin))) |
70 | 37, 68, 69 | mpbir2and 959 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((invg‘𝑃)‘𝑎) ∈ 𝐻) |
71 | 1, 2, 3, 16, 23, 30, 70, 31 | issubgrpd2 17433 |
1
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝑃)) |