Metamath Proof Explorer

Theorem xpsmnd0

Description: The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025)

Ref Expression
Hypothesis xpsmnd0.t 
|- T = ( R Xs. S )
Assertion xpsmnd0 
|- ( ( R e. Mnd /\ S e. Mnd ) -> ( 0g ` T ) = <. ( 0g ` R ) , ( 0g ` S ) >. )

Proof

Step Hyp Ref Expression
1 xpsmnd0.t 
 |-  T = ( R Xs. S )
2 eqid 
 |-  ( Base ` T ) = ( Base ` T )
3 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
4 eqid 
 |-  ( +g ` T ) = ( +g ` T )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 5 6 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
8 7 adantr 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( 0g ` R ) e. ( Base ` R ) )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
11 9 10 mndidcl 
 |-  ( S e. Mnd -> ( 0g ` S ) e. ( Base ` S ) )
12 11 adantl 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( 0g ` S ) e. ( Base ` S ) )
13 8 12 opelxpd 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> <. ( 0g ` R ) , ( 0g ` S ) >. e. ( ( Base ` R ) X. ( Base ` S ) ) )
14 simpl 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> R e. Mnd )
15 simpr 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> S e. Mnd )
16 1 5 9 14 15 xpsbas 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( ( Base ` R ) X. ( Base ` S ) ) = ( Base ` T ) )
17 13 16 eleqtrd 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> <. ( 0g ` R ) , ( 0g ` S ) >. e. ( Base ` T ) )
18 16 eleq2d 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( x e. ( ( Base ` R ) X. ( Base ` S ) ) <-> x e. ( Base ` T ) ) )
19 elxp2 
 |-  ( x e. ( ( Base ` R ) X. ( Base ` S ) ) <-> E. a e. ( Base ` R ) E. b e. ( Base ` S ) x = <. a , b >. )
20 14 adantr 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> R e. Mnd )
21 15 adantr 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> S e. Mnd )
22 8 adantr 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( 0g ` R ) e. ( Base ` R ) )
23 12 adantr 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( 0g ` S ) e. ( Base ` S ) )
24 simpl 
 |-  ( ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) -> a e. ( Base ` R ) )
25 24 adantl 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> a e. ( Base ` R ) )
26 simpr 
 |-  ( ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) -> b e. ( Base ` S ) )
27 26 adantl 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> b e. ( Base ` S ) )
28 eqid 
 |-  ( +g ` R ) = ( +g ` R )
29 5 28 mndcl 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. ( Base ` R ) /\ a e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) a ) e. ( Base ` R ) )
30 20 22 25 29 syl3anc 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( ( 0g ` R ) ( +g ` R ) a ) e. ( Base ` R ) )
31 eqid 
 |-  ( +g ` S ) = ( +g ` S )
32 9 31 mndcl 
 |-  ( ( S e. Mnd /\ ( 0g ` S ) e. ( Base ` S ) /\ b e. ( Base ` S ) ) -> ( ( 0g ` S ) ( +g ` S ) b ) e. ( Base ` S ) )
33 21 23 27 32 syl3anc 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( ( 0g ` S ) ( +g ` S ) b ) e. ( Base ` S ) )
34 1 5 9 20 21 22 23 25 27 30 33 28 31 4 xpsadd 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) <. a , b >. ) = <. ( ( 0g ` R ) ( +g ` R ) a ) , ( ( 0g ` S ) ( +g ` S ) b ) >. )
35 5 28 6 mndlid 
 |-  ( ( R e. Mnd /\ a e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) a ) = a )
36 14 24 35 syl2an 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( ( 0g ` R ) ( +g ` R ) a ) = a )
37 9 31 10 mndlid 
 |-  ( ( S e. Mnd /\ b e. ( Base ` S ) ) -> ( ( 0g ` S ) ( +g ` S ) b ) = b )
38 15 26 37 syl2an 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( ( 0g ` S ) ( +g ` S ) b ) = b )
39 36 38 opeq12d 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> <. ( ( 0g ` R ) ( +g ` R ) a ) , ( ( 0g ` S ) ( +g ` S ) b ) >. = <. a , b >. )
40 34 39 eqtrd 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) <. a , b >. ) = <. a , b >. )
41 oveq2 
 |-  ( x = <. a , b >. -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) <. a , b >. ) )
42 id 
 |-  ( x = <. a , b >. -> x = <. a , b >. )
43 41 42 eqeq12d 
 |-  ( x = <. a , b >. -> ( ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = x <-> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) <. a , b >. ) = <. a , b >. ) )
44 40 43 syl5ibrcom 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( x = <. a , b >. -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = x ) )
45 44 rexlimdvva 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( E. a e. ( Base ` R ) E. b e. ( Base ` S ) x = <. a , b >. -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = x ) )
46 19 45 biimtrid 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( x e. ( ( Base ` R ) X. ( Base ` S ) ) -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = x ) )
47 18 46 sylbird 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( x e. ( Base ` T ) -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = x ) )
48 47 imp 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ x e. ( Base ` T ) ) -> ( <. ( 0g ` R ) , ( 0g ` S ) >. ( +g ` T ) x ) = x )
49 5 28 mndcl 
 |-  ( ( R e. Mnd /\ a e. ( Base ` R ) /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( a ( +g ` R ) ( 0g ` R ) ) e. ( Base ` R ) )
50 20 25 22 49 syl3anc 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( a ( +g ` R ) ( 0g ` R ) ) e. ( Base ` R ) )
51 9 31 mndcl 
 |-  ( ( S e. Mnd /\ b e. ( Base ` S ) /\ ( 0g ` S ) e. ( Base ` S ) ) -> ( b ( +g ` S ) ( 0g ` S ) ) e. ( Base ` S ) )
52 21 27 23 51 syl3anc 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( b ( +g ` S ) ( 0g ` S ) ) e. ( Base ` S ) )
53 1 5 9 20 21 25 27 22 23 50 52 28 31 4 xpsadd 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( <. a , b >. ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = <. ( a ( +g ` R ) ( 0g ` R ) ) , ( b ( +g ` S ) ( 0g ` S ) ) >. )
54 5 28 6 mndrid 
 |-  ( ( R e. Mnd /\ a e. ( Base ` R ) ) -> ( a ( +g ` R ) ( 0g ` R ) ) = a )
55 14 24 54 syl2an 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( a ( +g ` R ) ( 0g ` R ) ) = a )
56 9 31 10 mndrid 
 |-  ( ( S e. Mnd /\ b e. ( Base ` S ) ) -> ( b ( +g ` S ) ( 0g ` S ) ) = b )
57 15 26 56 syl2an 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( b ( +g ` S ) ( 0g ` S ) ) = b )
58 55 57 opeq12d 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> <. ( a ( +g ` R ) ( 0g ` R ) ) , ( b ( +g ` S ) ( 0g ` S ) ) >. = <. a , b >. )
59 53 58 eqtrd 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( <. a , b >. ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = <. a , b >. )
60 oveq1 
 |-  ( x = <. a , b >. -> ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = ( <. a , b >. ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) )
61 60 42 eqeq12d 
 |-  ( x = <. a , b >. -> ( ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = x <-> ( <. a , b >. ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = <. a , b >. ) )
62 59 61 syl5ibrcom 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` S ) ) ) -> ( x = <. a , b >. -> ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = x ) )
63 62 rexlimdvva 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( E. a e. ( Base ` R ) E. b e. ( Base ` S ) x = <. a , b >. -> ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = x ) )
64 19 63 biimtrid 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( x e. ( ( Base ` R ) X. ( Base ` S ) ) -> ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = x ) )
65 18 64 sylbird 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( x e. ( Base ` T ) -> ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = x ) )
66 65 imp 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ x e. ( Base ` T ) ) -> ( x ( +g ` T ) <. ( 0g ` R ) , ( 0g ` S ) >. ) = x )
67 2 3 4 17 48 66 ismgmid2 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> <. ( 0g ` R ) , ( 0g ` S ) >. = ( 0g ` T ) )
68 67 eqcomd 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( 0g ` T ) = <. ( 0g ` R ) , ( 0g ` S ) >. )