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 ‘ 𝐿 ) )