Theorem sgrp2nmndlem3

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

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

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		df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
8		eqeq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 = 𝑥 ↔ 𝐴 = 𝐵 ) )
9	8	adantr	⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) → ( 𝐴 = 𝑥 ↔ 𝐴 = 𝐵 ) )
10		eqcom	⊢ ( 𝐴 = 𝑥 ↔ 𝑥 = 𝐴 )
11	9 10	bitr3di	⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) → ( 𝐴 = 𝐵 ↔ 𝑥 = 𝐴 ) )
12	11	notbid	⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) → ( ¬ 𝐴 = 𝐵 ↔ ¬ 𝑥 = 𝐴 ) )
13	12	biimpcd	⊢ ( ¬ 𝐴 = 𝐵 → ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) → ¬ 𝑥 = 𝐴 ) )
14	7 13	sylbi	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) → ¬ 𝑥 = 𝐴 ) )
15	14	3ad2ant3	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) → ¬ 𝑥 = 𝐴 ) )
16	15	imp	⊢ ( ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ) → ¬ 𝑥 = 𝐴 )
17	16	iffalsed	⊢ ( ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ) → if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) = 𝐵 )
18		simp2	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑆 )
19		simp1	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ∈ 𝑆 )
20	6 17 18 19 18	ovmpod	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ⚬ 𝐶 ) = 𝐵 )