Step |
Hyp |
Ref |
Expression |
1 |
|
prdscmnd.y |
⊢ 𝑌 = ( 𝑆 Xs 𝑅 ) |
2 |
|
prdscmnd.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
3 |
|
prdscmnd.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) |
4 |
|
prdsgabld.r |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Abel ) |
5 |
|
ablgrp |
⊢ ( 𝑎 ∈ Abel → 𝑎 ∈ Grp ) |
6 |
5
|
ssriv |
⊢ Abel ⊆ Grp |
7 |
|
fss |
⊢ ( ( 𝑅 : 𝐼 ⟶ Abel ∧ Abel ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp ) |
8 |
4 6 7
|
sylancl |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp ) |
9 |
1 2 3 8
|
prdsgrpd |
⊢ ( 𝜑 → 𝑌 ∈ Grp ) |
10 |
|
ablcmn |
⊢ ( 𝑎 ∈ Abel → 𝑎 ∈ CMnd ) |
11 |
10
|
ssriv |
⊢ Abel ⊆ CMnd |
12 |
|
fss |
⊢ ( ( 𝑅 : 𝐼 ⟶ Abel ∧ Abel ⊆ CMnd ) → 𝑅 : 𝐼 ⟶ CMnd ) |
13 |
4 11 12
|
sylancl |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ CMnd ) |
14 |
1 2 3 13
|
prdscmnd |
⊢ ( 𝜑 → 𝑌 ∈ CMnd ) |
15 |
|
isabl |
⊢ ( 𝑌 ∈ Abel ↔ ( 𝑌 ∈ Grp ∧ 𝑌 ∈ CMnd ) ) |
16 |
9 14 15
|
sylanbrc |
⊢ ( 𝜑 → 𝑌 ∈ Abel ) |