Metamath Proof Explorer

Theorem prdsinvgd

Description: Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsgrpd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsgrpd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsgrpd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsgrpd.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
prdsinvgd.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsinvgd.n ⊢ 𝑁 = ( invg ‘ 𝑌 )
prdsinvgd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion prdsinvgd ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) )

Proof

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 ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) )