Metamath Proof Explorer

Theorem xpsinv

Description: Value of the negation operation in a binary structure product. (Contributed by AV, 18-Mar-2025)

Ref Expression
Hypotheses xpsinv.t 
|- T = ( R Xs. S )
xpsinv.x 
|- X = ( Base ` R )
xpsinv.y 
|- Y = ( Base ` S )
xpsinv.r 
|- ( ph -> R e. Grp )
xpsinv.s 
|- ( ph -> S e. Grp )
xpsinv.a 
|- ( ph -> A e. X )
xpsinv.b 
|- ( ph -> B e. Y )
xpsinv.m 
|- M = ( invg ` R )
xpsinv.n 
|- N = ( invg ` S )
xpsinv.i 
|- I = ( invg ` T )
Assertion xpsinv 
|- ( ph -> ( I ` <. A , B >. ) = <. ( M ` A ) , ( N ` B ) >. )

Proof

Step Hyp Ref Expression
1 xpsinv.t 
 |-  T = ( R Xs. S )
2 xpsinv.x 
 |-  X = ( Base ` R )
3 xpsinv.y 
 |-  Y = ( Base ` S )
4 xpsinv.r 
 |-  ( ph -> R e. Grp )
5 xpsinv.s 
 |-  ( ph -> S e. Grp )
6 xpsinv.a 
 |-  ( ph -> A e. X )
7 xpsinv.b 
 |-  ( ph -> B e. Y )
8 xpsinv.m 
 |-  M = ( invg ` R )
9 xpsinv.n 
 |-  N = ( invg ` S )
10 xpsinv.i 
 |-  I = ( invg ` T )
11 eqid 
 |-  ( +g ` R ) = ( +g ` R )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 2 11 12 8 4 6 grplinvd 
 |-  ( ph -> ( ( M ` A ) ( +g ` R ) A ) = ( 0g ` R ) )
14 eqid 
 |-  ( +g ` S ) = ( +g ` S )
15 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
16 3 14 15 9 5 7 grplinvd 
 |-  ( ph -> ( ( N ` B ) ( +g ` S ) B ) = ( 0g ` S ) )
17 13 16 opeq12d 
 |-  ( ph -> <. ( ( M ` A ) ( +g ` R ) A ) , ( ( N ` B ) ( +g ` S ) B ) >. = <. ( 0g ` R ) , ( 0g ` S ) >. )
18 2 8 4 6 grpinvcld 
 |-  ( ph -> ( M ` A ) e. X )
19 3 9 5 7 grpinvcld 
 |-  ( ph -> ( N ` B ) e. Y )
20 2 11 4 18 6 grpcld 
 |-  ( ph -> ( ( M ` A ) ( +g ` R ) A ) e. X )
21 3 14 5 19 7 grpcld 
 |-  ( ph -> ( ( N ` B ) ( +g ` S ) B ) e. Y )
22 eqid 
 |-  ( +g ` T ) = ( +g ` T )
23 1 2 3 4 5 18 19 6 7 20 21 11 14 22 xpsadd 
 |-  ( ph -> ( <. ( M ` A ) , ( N ` B ) >. ( +g ` T ) <. A , B >. ) = <. ( ( M ` A ) ( +g ` R ) A ) , ( ( N ` B ) ( +g ` S ) B ) >. )
24 4 grpmndd 
 |-  ( ph -> R e. Mnd )
25 5 grpmndd 
 |-  ( ph -> S e. Mnd )
26 1 xpsmnd0 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( 0g ` T ) = <. ( 0g ` R ) , ( 0g ` S ) >. )
27 24 25 26 syl2anc 
 |-  ( ph -> ( 0g ` T ) = <. ( 0g ` R ) , ( 0g ` S ) >. )
28 17 23 27 3eqtr4d 
 |-  ( ph -> ( <. ( M ` A ) , ( N ` B ) >. ( +g ` T ) <. A , B >. ) = ( 0g ` T ) )
29 1 xpsgrp 
 |-  ( ( R e. Grp /\ S e. Grp ) -> T e. Grp )
30 4 5 29 syl2anc 
 |-  ( ph -> T e. Grp )
31 6 7 opelxpd 
 |-  ( ph -> <. A , B >. e. ( X X. Y ) )
32 1 2 3 4 5 xpsbas 
 |-  ( ph -> ( X X. Y ) = ( Base ` T ) )
33 31 32 eleqtrd 
 |-  ( ph -> <. A , B >. e. ( Base ` T ) )
34 18 19 opelxpd 
 |-  ( ph -> <. ( M ` A ) , ( N ` B ) >. e. ( X X. Y ) )
35 34 32 eleqtrd 
 |-  ( ph -> <. ( M ` A ) , ( N ` B ) >. e. ( Base ` T ) )
36 eqid 
 |-  ( Base ` T ) = ( Base ` T )
37 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
38 36 22 37 10 grpinvid2 
 |-  ( ( T e. Grp /\ <. A , B >. e. ( Base ` T ) /\ <. ( M ` A ) , ( N ` B ) >. e. ( Base ` T ) ) -> ( ( I ` <. A , B >. ) = <. ( M ` A ) , ( N ` B ) >. <-> ( <. ( M ` A ) , ( N ` B ) >. ( +g ` T ) <. A , B >. ) = ( 0g ` T ) ) )
39 30 33 35 38 syl3anc 
 |-  ( ph -> ( ( I ` <. A , B >. ) = <. ( M ` A ) , ( N ` B ) >. <-> ( <. ( M ` A ) , ( N ` B ) >. ( +g ` T ) <. A , B >. ) = ( 0g ` T ) ) )
40 28 39 mpbird 
 |-  ( ph -> ( I ` <. A , B >. ) = <. ( M ` A ) , ( N ` B ) >. )