Step |
Hyp |
Ref |
Expression |
1 |
|
dsmmsubg.p |
⊢ 𝑃 = ( 𝑆 Xs 𝑅 ) |
2 |
|
dsmmsubg.h |
⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) |
3 |
|
dsmmsubg.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
4 |
|
dsmmsubg.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) |
5 |
|
dsmmsubg.r |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp ) |
6 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑃 ↾s 𝐻 ) = ( 𝑃 ↾s 𝐻 ) ) |
7 |
|
eqidd |
⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) ) |
8 |
|
eqidd |
⊢ ( 𝜑 → ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) ) |
9 |
|
fex |
⊢ ( ( 𝑅 : 𝐼 ⟶ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V ) |
10 |
5 3 9
|
syl2anc |
⊢ ( 𝜑 → 𝑅 ∈ V ) |
11 |
|
eqid |
⊢ { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } = { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } |
12 |
11
|
dsmmbase |
⊢ ( 𝑅 ∈ V → { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) |
13 |
10 12
|
syl |
⊢ ( 𝜑 → { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) |
14 |
|
ssrab2 |
⊢ { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) |
15 |
13 14
|
eqsstrrdi |
⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) |
16 |
1
|
fveq2i |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) ) |
17 |
15 2 16
|
3sstr4g |
⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝑃 ) ) |
18 |
|
grpmnd |
⊢ ( 𝑎 ∈ Grp → 𝑎 ∈ Mnd ) |
19 |
18
|
ssriv |
⊢ Grp ⊆ Mnd |
20 |
|
fss |
⊢ ( ( 𝑅 : 𝐼 ⟶ Grp ∧ Grp ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd ) |
21 |
5 19 20
|
sylancl |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd ) |
22 |
|
eqid |
⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) |
23 |
1 2 3 4 21 22
|
dsmm0cl |
⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝐻 ) |
24 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝐼 ∈ 𝑊 ) |
25 |
4
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑆 ∈ 𝑉 ) |
26 |
21
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑅 : 𝐼 ⟶ Mnd ) |
27 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑎 ∈ 𝐻 ) |
28 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑏 ∈ 𝐻 ) |
29 |
|
eqid |
⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) |
30 |
1 2 24 25 26 27 28 29
|
dsmmacl |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 ) |
31 |
1 3 4 5
|
prdsgrpd |
⊢ ( 𝜑 → 𝑃 ∈ Grp ) |
32 |
31
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑃 ∈ Grp ) |
33 |
17
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ ( Base ‘ 𝑃 ) ) |
34 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
35 |
|
eqid |
⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 ) |
36 |
34 35
|
grpinvcl |
⊢ ( ( 𝑃 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝑃 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑃 ) ) |
37 |
32 33 36
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑃 ) ) |
38 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ 𝐻 ) |
39 |
|
eqid |
⊢ ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 ⊕m 𝑅 ) |
40 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐼 ∈ 𝑊 ) |
41 |
5
|
ffnd |
⊢ ( 𝜑 → 𝑅 Fn 𝐼 ) |
42 |
41
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑅 Fn 𝐼 ) |
43 |
1 39 34 2 40 42
|
dsmmelbas |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑎 ∈ 𝐻 ↔ ( 𝑎 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) ) ) |
44 |
38 43
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑎 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) ) |
45 |
44
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) |
46 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 ) |
47 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 ) |
48 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑅 : 𝐼 ⟶ Grp ) |
49 |
33
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑃 ) ) |
50 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑏 ∈ 𝐼 ) |
51 |
1 46 47 48 34 35 49 50
|
prdsinvgd2 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) |
52 |
51
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) |
53 |
|
fveq2 |
⊢ ( ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) |
54 |
53
|
ad2antll |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) |
55 |
5
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑏 ) ∈ Grp ) |
56 |
55
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑏 ) ∈ Grp ) |
57 |
|
eqid |
⊢ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) |
58 |
|
eqid |
⊢ ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) = ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) |
59 |
57 58
|
grpinvid |
⊢ ( ( 𝑅 ‘ 𝑏 ) ∈ Grp → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) |
60 |
56 59
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) |
61 |
60
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) |
62 |
52 54 61
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) |
63 |
62
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) |
64 |
63
|
necon3d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) → ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) |
65 |
64
|
ss2rabdv |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → { 𝑏 ∈ 𝐼 ∣ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ⊆ { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ) |
66 |
45 65
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → { 𝑏 ∈ 𝐼 ∣ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) |
67 |
1 39 34 2 40 42
|
dsmmelbas |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ 𝐻 ↔ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑏 ∈ 𝐼 ∣ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) ) ) |
68 |
37 66 67
|
mpbir2and |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ 𝐻 ) |
69 |
6 7 8 17 23 30 68 31
|
issubgrpd2 |
⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝑃 ) ) |