Theorem sgrp2nmndlem2

Description: Lemma 2 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	sgrp2nmndlem2	|- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A )

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	|- ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) )
7		iftrue	|- ( x = A -> if ( x = A , A , B ) = A )
8	7	ad2antrl	|- ( ( ( A e. S /\ C e. S ) /\ ( x = A /\ y = C ) ) -> if ( x = A , A , B ) = A )
9		simpl	|- ( ( A e. S /\ C e. S ) -> A e. S )
10		simpr	|- ( ( A e. S /\ C e. S ) -> C e. S )
11	6 8 9 10 9	ovmpod	|- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A )