Metamath Proof Explorer

Theorem copissgrp

Description: A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020)

Ref Expression
Hypotheses copissgrp.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
copissgrp.p ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
copissgrp.n ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
copissgrp.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion copissgrp ( 𝜑 → 𝑀 ∈ Smgrp )

Proof

Step Hyp Ref Expression
1 copissgrp.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 copissgrp.p ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3 copissgrp.n ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
4 copissgrp.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
5 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
6 1 2 3 5 opmpoismgm ⊢ ( 𝜑 → 𝑀 ∈ Mgm )
7 eqidd ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
8 eqidd ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝑐 ) ) → 𝐶 = 𝐶 )
9 simpl ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
10 simpr3 ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ 𝐵 )
11 7 8 9 10 9 ovmpod ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐶 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
12 eqidd ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝐶 ) ) → 𝐶 = 𝐶 )
13 simpr1 ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
14 7 12 13 9 9 ovmpod ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐶 ) = 𝐶 )
15 11 14 eqtr4d ⊢ ( ( 𝐶 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐶 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐶 ) )
16 4 15 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐶 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐶 ) )
17 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
18 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → 𝐶 = 𝐶 )
19 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
20 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
21 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
22 17 18 19 20 21 ovmpod ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) = 𝐶 )
23 22 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( 𝐶 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) )
24 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) ) → 𝐶 = 𝐶 )
25 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ 𝐵 )
26 17 24 20 25 21 ovmpod ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
27 26 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) = ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝐶 ) )
28 16 23 27 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) )
29 28 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) )
30 2 eqcomi ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( +g ‘ 𝑀 )
31 1 30 issgrp ⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ) )
32 6 29 31 sylanbrc ⊢ ( 𝜑 → 𝑀 ∈ Smgrp )