This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpinvpropd

Description: If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014) (Revised by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypotheses grpinvpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
grpinvpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
grpinvpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
Assertion grpinvpropd ( 𝜑 → ( invg ‘ 𝐾 ) = ( invg ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 grpinvpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 grpinvpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 grpinvpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 1 2 3 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
5 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
6 3 5 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
7 6 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
8 7 riotabidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) = ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
9 8 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) ) )
10 1 riotaeqdv ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) = ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) )
11 1 10 mpteq12dv ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) ) )
12 2 riotaeqdv ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) = ( ℩ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
13 2 12 mpteq12dv ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) ) )
14 9 11 13 3eqtr3d ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) ) )
15 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
17 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
18 eqid ⊢ ( invg ‘ 𝐾 ) = ( invg ‘ 𝐾 )
19 15 16 17 18 grpinvfval ⊢ ( invg ‘ 𝐾 ) = ( 𝑦 ∈ ( Base ‘ 𝐾 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 0g ‘ 𝐾 ) ) )
20 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
21 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
22 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
23 eqid ⊢ ( invg ‘ 𝐿 ) = ( invg ‘ 𝐿 )
24 20 21 22 23 grpinvfval ⊢ ( invg ‘ 𝐿 ) = ( 𝑦 ∈ ( Base ‘ 𝐿 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = ( 0g ‘ 𝐿 ) ) )
25 14 19 24 3eqtr4g ⊢ ( 𝜑 → ( invg ‘ 𝐾 ) = ( invg ‘ 𝐿 ) )