Metamath Proof Explorer

Theorem xpsgrpsub

Description: Value of the subtraction operation in a binary structure product of groups. (Contributed by AV, 24-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 )
xpsgrpsub.c 
|- ( ph -> C e. X )
xpsgrpsub.d 
|- ( ph -> D e. Y )
xpsgrpsub.m 
|- .x. = ( -g ` R )
xpsgrpsub.n 
|- .X. = ( -g ` S )
xpsgrpsub.o 
|- .- = ( -g ` T )
Assertion xpsgrpsub 
|- ( ph -> ( <. A , B >. .- <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )

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 xpsgrpsub.c 
 |-  ( ph -> C e. X )
9 xpsgrpsub.d 
 |-  ( ph -> D e. Y )
10 xpsgrpsub.m 
 |-  .x. = ( -g ` R )
11 xpsgrpsub.n 
 |-  .X. = ( -g ` S )
12 xpsgrpsub.o 
 |-  .- = ( -g ` T )
13 2 10 grpsubcl 
 |-  ( ( R e. Grp /\ A e. X /\ C e. X ) -> ( A .x. C ) e. X )
14 4 6 8 13 syl3anc 
 |-  ( ph -> ( A .x. C ) e. X )
15 3 11 grpsubcl 
 |-  ( ( S e. Grp /\ B e. Y /\ D e. Y ) -> ( B .X. D ) e. Y )
16 5 7 9 15 syl3anc 
 |-  ( ph -> ( B .X. D ) e. Y )
17 eqid 
 |-  ( +g ` R ) = ( +g ` R )
18 2 17 4 14 8 grpcld 
 |-  ( ph -> ( ( A .x. C ) ( +g ` R ) C ) e. X )
19 eqid 
 |-  ( +g ` S ) = ( +g ` S )
20 3 19 5 16 9 grpcld 
 |-  ( ph -> ( ( B .X. D ) ( +g ` S ) D ) e. Y )
21 eqid 
 |-  ( +g ` T ) = ( +g ` T )
22 1 2 3 4 5 14 16 8 9 18 20 17 19 21 xpsadd 
 |-  ( ph -> ( <. ( A .x. C ) , ( B .X. D ) >. ( +g ` T ) <. C , D >. ) = <. ( ( A .x. C ) ( +g ` R ) C ) , ( ( B .X. D ) ( +g ` S ) D ) >. )
23 2 17 10 grpnpcan 
 |-  ( ( R e. Grp /\ A e. X /\ C e. X ) -> ( ( A .x. C ) ( +g ` R ) C ) = A )
24 4 6 8 23 syl3anc 
 |-  ( ph -> ( ( A .x. C ) ( +g ` R ) C ) = A )
25 3 19 11 grpnpcan 
 |-  ( ( S e. Grp /\ B e. Y /\ D e. Y ) -> ( ( B .X. D ) ( +g ` S ) D ) = B )
26 5 7 9 25 syl3anc 
 |-  ( ph -> ( ( B .X. D ) ( +g ` S ) D ) = B )
27 24 26 opeq12d 
 |-  ( ph -> <. ( ( A .x. C ) ( +g ` R ) C ) , ( ( B .X. D ) ( +g ` S ) D ) >. = <. A , B >. )
28 22 27 eqtrd 
 |-  ( ph -> ( <. ( A .x. C ) , ( B .X. D ) >. ( +g ` T ) <. C , D >. ) = <. A , B >. )
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 8 9 opelxpd 
 |-  ( ph -> <. C , D >. e. ( X X. Y ) )
35 34 32 eleqtrd 
 |-  ( ph -> <. C , D >. e. ( Base ` T ) )
36 14 16 opelxpd 
 |-  ( ph -> <. ( A .x. C ) , ( B .X. D ) >. e. ( X X. Y ) )
37 36 32 eleqtrd 
 |-  ( ph -> <. ( A .x. C ) , ( B .X. D ) >. e. ( Base ` T ) )
38 eqid 
 |-  ( Base ` T ) = ( Base ` T )
39 38 21 12 grpsubadd 
 |-  ( ( T e. Grp /\ ( <. A , B >. e. ( Base ` T ) /\ <. C , D >. e. ( Base ` T ) /\ <. ( A .x. C ) , ( B .X. D ) >. e. ( Base ` T ) ) ) -> ( ( <. A , B >. .- <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. <-> ( <. ( A .x. C ) , ( B .X. D ) >. ( +g ` T ) <. C , D >. ) = <. A , B >. ) )
40 30 33 35 37 39 syl13anc 
 |-  ( ph -> ( ( <. A , B >. .- <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. <-> ( <. ( A .x. C ) , ( B .X. D ) >. ( +g ` T ) <. C , D >. ) = <. A , B >. ) )
41 28 40 mpbird 
 |-  ( ph -> ( <. A , B >. .- <. C , D >. ) = <. ( A .x. C ) , ( B .X. D ) >. )