Metamath Proof Explorer


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 + M = x S , y S if x = A A B
sgrp2nmnd.p No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion sgrp2nmndlem2 Could not format assertion : No typesetting found for |- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) with typecode |-

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s S = A B
2 mgm2nsgrp.b Base M = S
3 sgrp2nmnd.o + M = x S , y S if x = A A B
4 sgrp2nmnd.p Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
5 4 3 eqtri Could not format .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) : No typesetting found for |- .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) with typecode |-
6 5 a1i Could not format ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) : No typesetting found for |- ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) with typecode |-
7 iftrue x = A if x = A A B = A
8 7 ad2antrl A S C S x = A y = C if x = A A B = A
9 simpl A S C S A S
10 simpr A S C S C S
11 6 8 9 10 9 ovmpod Could not format ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) : No typesetting found for |- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) with typecode |-