Theorem mgm2nsgrplem2

Description: Lemma 2 for mgm2nsgrp . (Contributed by AV, 27-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	mgm2nsgrplem2	|- ( ( A e. V /\ B e. W ) -> ( ( A .o. A ) .o. B ) = A )

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		ifeq1	|- ( B = A -> if ( ( x = A /\ y = A ) , B , A ) = if ( ( x = A /\ y = A ) , A , A ) )
12		ifid	|- if ( ( x = A /\ y = A ) , A , A ) = A
13	11 12	eqtrdi	|- ( B = A -> if ( ( x = A /\ y = A ) , B , A ) = A )
14	13	a1d	|- ( B = A -> ( y = B -> if ( ( x = A /\ y = A ) , B , A ) = A ) )
15		eqeq1	|- ( y = B -> ( y = A <-> B = A ) )
16	15	bicomd	|- ( y = B -> ( B = A <-> y = A ) )
17	16	notbid	|- ( y = B -> ( -. B = A <-> -. y = A ) )
18	17	biimpac	|- ( ( -. B = A /\ y = B ) -> -. y = A )
19	18	intnand	|- ( ( -. B = A /\ y = B ) -> -. ( x = A /\ y = A ) )
20	19	iffalsed	|- ( ( -. B = A /\ y = B ) -> if ( ( x = A /\ y = A ) , B , A ) = A )
21	20	ex	|- ( -. B = A -> ( y = B -> if ( ( x = A /\ y = A ) , B , A ) = A ) )
22	14 21	pm2.61i	|- ( y = B -> if ( ( x = A /\ y = A ) , B , A ) = A )
23	22	ad2antll	|- ( ( ( A e. S /\ B e. S ) /\ ( x = ( A .o. A ) /\ y = B ) ) -> if ( ( x = A /\ y = A ) , B , A ) = A )
24		iftrue	|- ( ( x = A /\ y = A ) -> if ( ( x = A /\ y = A ) , B , A ) = B )
25	24	adantl	|- ( ( ( A e. S /\ B e. S ) /\ ( x = A /\ y = A ) ) -> if ( ( x = A /\ y = A ) , B , A ) = B )
26		simpl	|- ( ( A e. S /\ B e. S ) -> A e. S )
27		simpr	|- ( ( A e. S /\ B e. S ) -> B e. S )
28	10 25 26 26 27	ovmpod	|- ( ( A e. S /\ B e. S ) -> ( A .o. A ) = B )
29	28 27	eqeltrd	|- ( ( A e. S /\ B e. S ) -> ( A .o. A ) e. S )
30	10 23 29 27 26	ovmpod	|- ( ( A e. S /\ B e. S ) -> ( ( A .o. A ) .o. B ) = A )
31	6 8 30	syl2an	|- ( ( A e. V /\ B e. W ) -> ( ( A .o. A ) .o. B ) = A )