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

Metamath Proof Explorer

Theorem grpidpropd

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 grpidpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 grpidpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 grpidpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 3 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ) )
5 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( +g ‘ 𝐾 ) 𝑤 ) = ( 𝑧 ( +g ‘ 𝐿 ) 𝑤 ) )
6 5 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) )
7 6 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) )
8 7 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ↔ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) )
9 4 8 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) )
10 9 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) )
11 10 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) )
12 11 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) ) )
13 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐾 ) ) )
14 1 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) )
15 13 14 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) ) )
16 2 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐿 ) ) )
17 2 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) )
18 16 17 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) ) )
19 12 15 18 3bitr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) ) )
20 19 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) ) )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
23 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
24 21 22 23 grpidval ⊢ ( 0g ‘ 𝐾 ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐾 ) 𝑥 ) = 𝑦 ) ) )
25 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
26 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
27 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
28 25 26 27 grpidval ⊢ ( 0g ‘ 𝐿 ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐿 ) 𝑥 ) = 𝑦 ) ) )
29 20 24 28 3eqtr4g ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )