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 ⊢ Y = S ⨉ 𝑠 R
prdsgrpd.i ⊢ φ → I ∈ W
prdsgrpd.s ⊢ φ → S ∈ V
prdsgrpd.r ⊢ φ → R : I ⟶ Grp
prdsinvgd.b ⊢ B = Base Y
prdsinvgd.n ⊢ N = inv g ⁡ Y
prdsinvgd.x ⊢ φ → X ∈ B
Assertion prdsinvgd ⊢ φ → N ⁡ X = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x

Proof

Step Hyp Ref Expression
1 prdsgrpd.y ⊢ Y = S ⨉ 𝑠 R
2 prdsgrpd.i ⊢ φ → I ∈ W
3 prdsgrpd.s ⊢ φ → S ∈ V
4 prdsgrpd.r ⊢ φ → R : I ⟶ Grp
5 prdsinvgd.b ⊢ B = Base Y
6 prdsinvgd.n ⊢ N = inv g ⁡ Y
7 prdsinvgd.x ⊢ φ → X ∈ B
8 eqid ⊢ + Y = + Y
9 3 elexd ⊢ φ → S ∈ V
10 2 elexd ⊢ φ → I ∈ V
11 eqid ⊢ 0 𝑔 ∘ R = 0 𝑔 ∘ R
12 eqid ⊢ x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x
13 1 5 8 9 10 4 7 11 12 prdsinvlem ⊢ φ → x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ∈ B ∧ x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x + Y X = 0 𝑔 ∘ R
14 13 simprd ⊢ φ → x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x + Y X = 0 𝑔 ∘ R
15 grpmnd ⊢ a ∈ Grp → a ∈ Mnd
16 15 ssriv ⊢ Grp ⊆ Mnd
17 fss ⊢ R : I ⟶ Grp ∧ Grp ⊆ Mnd → R : I ⟶ Mnd
18 4 16 17 sylancl ⊢ φ → R : I ⟶ Mnd
19 1 2 3 18 prds0g ⊢ φ → 0 𝑔 ∘ R = 0 Y
20 14 19 eqtrd ⊢ φ → x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x + Y X = 0 Y
21 1 2 3 4 prdsgrpd ⊢ φ → Y ∈ Grp
22 13 simpld ⊢ φ → x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ∈ B
23 eqid ⊢ 0 Y = 0 Y
24 5 8 23 6 grpinvid2 ⊢ Y ∈ Grp ∧ X ∈ B ∧ x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ∈ B → N ⁡ X = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ↔ x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x + Y X = 0 Y
25 21 7 22 24 syl3anc ⊢ φ → N ⁡ X = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ↔ x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x + Y X = 0 Y
26 20 25 mpbird ⊢ φ → N ⁡ X = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x