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