Step |
Hyp |
Ref |
Expression |
1 |
|
prdsgrpd.y |
⊢ 𝑌 = ( 𝑆 Xs 𝑅 ) |
2 |
|
prdsgrpd.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
3 |
|
prdsgrpd.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) |
4 |
|
prdsgrpd.r |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp ) |
5 |
|
prdsinvgd.b |
⊢ 𝐵 = ( Base ‘ 𝑌 ) |
6 |
|
prdsinvgd.n |
⊢ 𝑁 = ( invg ‘ 𝑌 ) |
7 |
|
prdsinvgd.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
8 |
|
eqid |
⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) |
9 |
3
|
elexd |
⊢ ( 𝜑 → 𝑆 ∈ V ) |
10 |
2
|
elexd |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
11 |
|
eqid |
⊢ ( 0g ∘ 𝑅 ) = ( 0g ∘ 𝑅 ) |
12 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) |
13 |
1 5 8 9 10 4 7 11 12
|
prdsinvlem |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ( +g ‘ 𝑌 ) 𝑋 ) = ( 0g ∘ 𝑅 ) ) ) |
14 |
13
|
simprd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ( +g ‘ 𝑌 ) 𝑋 ) = ( 0g ∘ 𝑅 ) ) |
15 |
|
grpmnd |
⊢ ( 𝑎 ∈ Grp → 𝑎 ∈ Mnd ) |
16 |
15
|
ssriv |
⊢ Grp ⊆ Mnd |
17 |
|
fss |
⊢ ( ( 𝑅 : 𝐼 ⟶ Grp ∧ Grp ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd ) |
18 |
4 16 17
|
sylancl |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd ) |
19 |
1 2 3 18
|
prds0g |
⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑌 ) ) |
20 |
14 19
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ( +g ‘ 𝑌 ) 𝑋 ) = ( 0g ‘ 𝑌 ) ) |
21 |
1 2 3 4
|
prdsgrpd |
⊢ ( 𝜑 → 𝑌 ∈ Grp ) |
22 |
13
|
simpld |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ∈ 𝐵 ) |
23 |
|
eqid |
⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 ) |
24 |
5 8 23 6
|
grpinvid2 |
⊢ ( ( 𝑌 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ( +g ‘ 𝑌 ) 𝑋 ) = ( 0g ‘ 𝑌 ) ) ) |
25 |
21 7 22 24
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ( +g ‘ 𝑌 ) 𝑋 ) = ( 0g ‘ 𝑌 ) ) ) |
26 |
20 25
|
mpbird |
⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ) |