Theorem sgrp2nmndlem3

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

	Ref	Expression
Hypotheses	mgm2nsgrp.s	|- S = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
	sgrp2nmnd.p	|- .o. = ( +g ` M )
Assertion	sgrp2nmndlem3	|- ( ( C e. S /\ B e. S /\ A =/= B ) -> ( B .o. C ) = B )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
4		sgrp2nmnd.p	|- .o. = ( +g ` M )
5	4 3	eqtri	|- .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) )
6	5	a1i	|- ( ( C e. S /\ B e. S /\ A =/= B ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) )
7		df-ne	|- ( A =/= B <-> -. A = B )
8		eqeq2	|- ( x = B -> ( A = x <-> A = B ) )
9	8	adantr	|- ( ( x = B /\ y = C ) -> ( A = x <-> A = B ) )
10		eqcom	|- ( A = x <-> x = A )
11	9 10	bitr3di	|- ( ( x = B /\ y = C ) -> ( A = B <-> x = A ) )
12	11	notbid	|- ( ( x = B /\ y = C ) -> ( -. A = B <-> -. x = A ) )
13	12	biimpcd	|- ( -. A = B -> ( ( x = B /\ y = C ) -> -. x = A ) )
14	7 13	sylbi	|- ( A =/= B -> ( ( x = B /\ y = C ) -> -. x = A ) )
15	14	3ad2ant3	|- ( ( C e. S /\ B e. S /\ A =/= B ) -> ( ( x = B /\ y = C ) -> -. x = A ) )
16	15	imp	|- ( ( ( C e. S /\ B e. S /\ A =/= B ) /\ ( x = B /\ y = C ) ) -> -. x = A )
17	16	iffalsed	|- ( ( ( C e. S /\ B e. S /\ A =/= B ) /\ ( x = B /\ y = C ) ) -> if ( x = A , A , B ) = B )
18		simp2	|- ( ( C e. S /\ B e. S /\ A =/= B ) -> B e. S )
19		simp1	|- ( ( C e. S /\ B e. S /\ A =/= B ) -> C e. S )
20	6 17 18 19 18	ovmpod	|- ( ( C e. S /\ B e. S /\ A =/= B ) -> ( B .o. C ) = B )