Theorem mgm2nsgrplem3

Description: Lemma 3 for mgm2nsgrp . (Contributed by AV, 28-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
4		mgm2nsgrp.p	|- .o. = ( +g ` M )
5		prid1g	|- ( A e. V -> A e. { A , B } )
6	5 1	eleqtrrdi	|- ( A e. V -> A e. S )
7		prid2g	|- ( B e. W -> B e. { A , B } )
8	7 1	eleqtrrdi	|- ( B e. W -> B e. S )
9	4 3	eqtri	|- .o. = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
10	9	a1i	|- ( ( A e. S /\ B e. S ) -> .o. = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) ) )
11		simprl	|- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> x = A )
12		simpr	|- ( ( x = A /\ y = ( A .o. B ) ) -> y = ( A .o. B ) )
13		ifeq1	|- ( B = A -> if ( ( x = A /\ y = A ) , B , A ) = if ( ( x = A /\ y = A ) , A , A ) )
14		ifid	|- if ( ( x = A /\ y = A ) , A , A ) = A
15	13 14	eqtrdi	|- ( B = A -> if ( ( x = A /\ y = A ) , B , A ) = A )
16	15	a1d	|- ( B = A -> ( ( x = A /\ y = B ) -> if ( ( x = A /\ y = A ) , B , A ) = A ) )
17		eqeq1	|- ( y = B -> ( y = A <-> B = A ) )
18	17	biimpcd	|- ( y = A -> ( y = B -> B = A ) )
19	18	adantl	|- ( ( x = A /\ y = A ) -> ( y = B -> B = A ) )
20	19	com12	|- ( y = B -> ( ( x = A /\ y = A ) -> B = A ) )
21	20	adantl	|- ( ( x = A /\ y = B ) -> ( ( x = A /\ y = A ) -> B = A ) )
22	21	con3d	|- ( ( x = A /\ y = B ) -> ( -. B = A -> -. ( x = A /\ y = A ) ) )
23	22	impcom	|- ( ( -. B = A /\ ( x = A /\ y = B ) ) -> -. ( x = A /\ y = A ) )
24	23	iffalsed	|- ( ( -. B = A /\ ( x = A /\ y = B ) ) -> if ( ( x = A /\ y = A ) , B , A ) = A )
25	24	ex	|- ( -. B = A -> ( ( x = A /\ y = B ) -> if ( ( x = A /\ y = A ) , B , A ) = A ) )
26	16 25	pm2.61i	|- ( ( x = A /\ y = B ) -> if ( ( x = A /\ y = A ) , B , A ) = A )
27	26	adantl	|- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = B ) ) -> if ( ( x = A /\ y = A ) , B , A ) = A )
28		simpl	|- ( ( A e. S /\ B e. S ) -> A e. S )
29		simpr	|- ( ( A e. S /\ B e. S ) -> B e. S )
30	10 27 28 29 28	ovmpod	|- ( ( A e. S /\ B e. S ) -> ( A .o. B ) = A )
31	12 30	sylan9eqr	|- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> y = A )
32	11 31	jca	|- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> ( x = A /\ y = A ) )
33	32	iftrued	|- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = ( A .o. B ) ) ) -> if ( ( x = A /\ y = A ) , B , A ) = B )
34	30 28	eqeltrd	|- ( ( A e. S /\ B e. S ) -> ( A .o. B ) e. S )
35	10 33 28 34 29	ovmpod	|- ( ( A e. S /\ B e. S ) -> ( A .o. ( A .o. B ) ) = B )
36	6 8 35	syl2an	|- ( ( A e. V /\ B e. W ) -> ( A .o. ( A .o. B ) ) = B )