| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2737 | . 2
⊢ (𝜑 → (𝑃 ↾s 𝐻) = (𝑃 ↾s 𝐻)) | 
| 2 |  | eqidd 2737 | . 2
⊢ (𝜑 → (0g‘𝑃) = (0g‘𝑃)) | 
| 3 |  | eqidd 2737 | . 2
⊢ (𝜑 → (+g‘𝑃) = (+g‘𝑃)) | 
| 4 |  | dsmmsubg.r | . . . . . 6
⊢ (𝜑 → 𝑅:𝐼⟶Grp) | 
| 5 |  | dsmmsubg.i | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 6 | 4, 5 | fexd 7248 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ V) | 
| 7 |  | eqid 2736 | . . . . . 6
⊢ {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} = {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} | 
| 8 | 7 | dsmmbase 21756 | . . . . 5
⊢ (𝑅 ∈ V → {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} = (Base‘(𝑆 ⊕m 𝑅))) | 
| 9 | 6, 8 | syl 17 | . . . 4
⊢ (𝜑 → {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} = (Base‘(𝑆 ⊕m 𝑅))) | 
| 10 |  | ssrab2 4079 | . . . 4
⊢ {𝑎 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑏 ∈ dom 𝑅 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin} ⊆ (Base‘(𝑆Xs𝑅)) | 
| 11 | 9, 10 | eqsstrrdi 4028 | . . 3
⊢ (𝜑 → (Base‘(𝑆 ⊕m 𝑅)) ⊆ (Base‘(𝑆Xs𝑅))) | 
| 12 |  | dsmmsubg.h | . . 3
⊢ 𝐻 = (Base‘(𝑆 ⊕m 𝑅)) | 
| 13 |  | dsmmsubg.p | . . . 4
⊢ 𝑃 = (𝑆Xs𝑅) | 
| 14 | 13 | fveq2i 6908 | . . 3
⊢
(Base‘𝑃) =
(Base‘(𝑆Xs𝑅)) | 
| 15 | 11, 12, 14 | 3sstr4g 4036 | . 2
⊢ (𝜑 → 𝐻 ⊆ (Base‘𝑃)) | 
| 16 |  | dsmmsubg.s | . . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) | 
| 17 |  | grpmnd 18959 | . . . . 5
⊢ (𝑎 ∈ Grp → 𝑎 ∈ Mnd) | 
| 18 | 17 | ssriv 3986 | . . . 4
⊢ Grp
⊆ Mnd | 
| 19 |  | fss 6751 | . . . 4
⊢ ((𝑅:𝐼⟶Grp ∧ Grp ⊆ Mnd) →
𝑅:𝐼⟶Mnd) | 
| 20 | 4, 18, 19 | sylancl 586 | . . 3
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) | 
| 21 |  | eqid 2736 | . . 3
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 22 | 13, 12, 5, 16, 20, 21 | dsmm0cl 21761 | . 2
⊢ (𝜑 → (0g‘𝑃) ∈ 𝐻) | 
| 23 | 5 | 3ad2ant1 1133 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝐼 ∈ 𝑊) | 
| 24 | 16 | 3ad2ant1 1133 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑆 ∈ 𝑉) | 
| 25 | 20 | 3ad2ant1 1133 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑅:𝐼⟶Mnd) | 
| 26 |  | simp2 1137 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑎 ∈ 𝐻) | 
| 27 |  | simp3 1138 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → 𝑏 ∈ 𝐻) | 
| 28 |  | eqid 2736 | . . 3
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 29 | 13, 12, 23, 24, 25, 26, 27, 28 | dsmmacl 21762 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻) → (𝑎(+g‘𝑃)𝑏) ∈ 𝐻) | 
| 30 | 13, 5, 16, 4 | prdsgrpd 19069 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 31 | 30 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑃 ∈ Grp) | 
| 32 | 15 | sselda 3982 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 ∈ (Base‘𝑃)) | 
| 33 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 34 |  | eqid 2736 | . . . . 5
⊢
(invg‘𝑃) = (invg‘𝑃) | 
| 35 | 33, 34 | grpinvcl 19006 | . . . 4
⊢ ((𝑃 ∈ Grp ∧ 𝑎 ∈ (Base‘𝑃)) →
((invg‘𝑃)‘𝑎) ∈ (Base‘𝑃)) | 
| 36 | 31, 32, 35 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((invg‘𝑃)‘𝑎) ∈ (Base‘𝑃)) | 
| 37 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑎 ∈ 𝐻) | 
| 38 |  | eqid 2736 | . . . . . . 7
⊢ (𝑆 ⊕m 𝑅) = (𝑆 ⊕m 𝑅) | 
| 39 | 5 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝐼 ∈ 𝑊) | 
| 40 | 4 | ffnd 6736 | . . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) | 
| 41 | 40 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → 𝑅 Fn 𝐼) | 
| 42 | 13, 38, 33, 12, 39, 41 | dsmmelbas 21760 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑎 ∈ 𝐻 ↔ (𝑎 ∈ (Base‘𝑃) ∧ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin))) | 
| 43 | 37, 42 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝑎 ∈ (Base‘𝑃) ∧ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin)) | 
| 44 | 43 | simprd 495 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin) | 
| 45 | 5 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝐼 ∈ 𝑊) | 
| 46 | 16 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑆 ∈ 𝑉) | 
| 47 | 4 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑅:𝐼⟶Grp) | 
| 48 | 32 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑃)) | 
| 49 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → 𝑏 ∈ 𝐼) | 
| 50 | 13, 45, 46, 47, 33, 34, 48, 49 | prdsinvgd2 21763 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → (((invg‘𝑃)‘𝑎)‘𝑏) = ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏))) | 
| 51 | 50 | adantrr 717 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → (((invg‘𝑃)‘𝑎)‘𝑏) = ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏))) | 
| 52 |  | fveq2 6905 | . . . . . . . . 9
⊢ ((𝑎‘𝑏) = (0g‘(𝑅‘𝑏)) → ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏)) = ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏)))) | 
| 53 | 52 | ad2antll 729 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → ((invg‘(𝑅‘𝑏))‘(𝑎‘𝑏)) = ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏)))) | 
| 54 | 4 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐼) → (𝑅‘𝑏) ∈ Grp) | 
| 55 | 54 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → (𝑅‘𝑏) ∈ Grp) | 
| 56 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0g‘(𝑅‘𝑏)) = (0g‘(𝑅‘𝑏)) | 
| 57 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(invg‘(𝑅‘𝑏)) = (invg‘(𝑅‘𝑏)) | 
| 58 | 56, 57 | grpinvid 19018 | . . . . . . . . . 10
⊢ ((𝑅‘𝑏) ∈ Grp →
((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏))) = (0g‘(𝑅‘𝑏))) | 
| 59 | 55, 58 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏))) = (0g‘(𝑅‘𝑏))) | 
| 60 | 59 | adantrr 717 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → ((invg‘(𝑅‘𝑏))‘(0g‘(𝑅‘𝑏))) = (0g‘(𝑅‘𝑏))) | 
| 61 | 51, 53, 60 | 3eqtrd 2780 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ (𝑏 ∈ 𝐼 ∧ (𝑎‘𝑏) = (0g‘(𝑅‘𝑏)))) → (((invg‘𝑃)‘𝑎)‘𝑏) = (0g‘(𝑅‘𝑏))) | 
| 62 | 61 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → ((𝑎‘𝑏) = (0g‘(𝑅‘𝑏)) → (((invg‘𝑃)‘𝑎)‘𝑏) = (0g‘(𝑅‘𝑏)))) | 
| 63 | 62 | necon3d 2960 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐻) ∧ 𝑏 ∈ 𝐼) → ((((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏)) → (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏)))) | 
| 64 | 63 | ss2rabdv 4075 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ⊆ {𝑏 ∈ 𝐼 ∣ (𝑎‘𝑏) ≠ (0g‘(𝑅‘𝑏))}) | 
| 65 | 44, 64 | ssfid 9302 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin) | 
| 66 | 13, 38, 33, 12, 39, 41 | dsmmelbas 21760 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (((invg‘𝑃)‘𝑎) ∈ 𝐻 ↔ (((invg‘𝑃)‘𝑎) ∈ (Base‘𝑃) ∧ {𝑏 ∈ 𝐼 ∣ (((invg‘𝑃)‘𝑎)‘𝑏) ≠ (0g‘(𝑅‘𝑏))} ∈ Fin))) | 
| 67 | 36, 65, 66 | mpbir2and 713 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → ((invg‘𝑃)‘𝑎) ∈ 𝐻) | 
| 68 | 1, 2, 3, 15, 22, 29, 67, 30 | issubgrpd2 19161 | 1
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝑃)) |