Proof of Theorem rabsubmgmd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssrab2 4080 | . . 3
⊢ {𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵 | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵) | 
| 3 |  | rabsubmgmd.th | . . . . . 6
⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃)) | 
| 4 | 3 | elrab 3692 | . . . . 5
⊢ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ↔ (𝑥 ∈ 𝐵 ∧ 𝜃)) | 
| 5 |  | rabsubmgmd.ta | . . . . . 6
⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏)) | 
| 6 | 5 | elrab 3692 | . . . . 5
⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ↔ (𝑦 ∈ 𝐵 ∧ 𝜏)) | 
| 7 | 4, 6 | anbi12i 628 | . . . 4
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ∧ 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) ↔ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) | 
| 8 |  | rabsubmgmd.et | . . . . 5
⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂)) | 
| 9 |  | rabsubmgmd.m | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ Mgm) | 
| 10 | 9 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝑀 ∈ Mgm) | 
| 11 |  | simprll 779 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝑥 ∈ 𝐵) | 
| 12 |  | simprrl 781 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝑦 ∈ 𝐵) | 
| 13 |  | rabsubmgmd.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑀) | 
| 14 |  | rabsubmgmd.p | . . . . . . 7
⊢  + =
(+g‘𝑀) | 
| 15 | 13, 14 | mgmcl 18656 | . . . . . 6
⊢ ((𝑀 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) | 
| 16 | 10, 11, 12, 15 | syl3anc 1373 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → (𝑥 + 𝑦) ∈ 𝐵) | 
| 17 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝜃) → 𝑥 ∈ 𝐵) | 
| 18 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝜏) → 𝑦 ∈ 𝐵) | 
| 19 | 17, 18 | anim12i 613 | . . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) | 
| 20 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝜃) → 𝜃) | 
| 21 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝜏) → 𝜏) | 
| 22 | 20, 21 | anim12i 613 | . . . . . . 7
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏)) → (𝜃 ∧ 𝜏)) | 
| 23 | 19, 22 | jca 511 | . . . . . 6
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏)) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) | 
| 24 |  | rabsubmgmd.cp | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂) | 
| 25 | 23, 24 | sylan2 593 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝜂) | 
| 26 | 8, 16, 25 | elrabd 3694 | . . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) | 
| 27 | 7, 26 | sylan2b 594 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ∧ 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓})) → (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) | 
| 28 | 27 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) | 
| 29 | 13, 14 | issubmgm 18715 | . . 3
⊢ (𝑀 ∈ Mgm → ({𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMgm‘𝑀) ↔ ({𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵 ∧ ∀𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}))) | 
| 30 | 9, 29 | syl 17 | . 2
⊢ (𝜑 → ({𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMgm‘𝑀) ↔ ({𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵 ∧ ∀𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}))) | 
| 31 | 2, 28, 30 | mpbir2and 713 | 1
⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMgm‘𝑀)) |