Theorem sgrp2nmndlem2

Description: Lemma 2 for sgrp2nmnd . (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Hypotheses	mgm2nsgrp.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
	mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
	sgrp2nmnd.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
	sgrp2nmnd.p	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	sgrp2nmndlem2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐶 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
2		mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
3		sgrp2nmnd.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
4		sgrp2nmnd.p	⊢ ⚬ = ( +g ‘ 𝑀 )
5	4 3	eqtri	⊢ ⚬ = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
6	5	a1i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ⚬ = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) ) )
7		iftrue	⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) = 𝐴 )
8	7	ad2antrl	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐶 ) ) → if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) = 𝐴 )
9		simpl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
10		simpr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝐶 ∈ 𝑆 )
11	6 8 9 10 9	ovmpod	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐶 ) = 𝐴 )