Metamath Proof Explorer

Theorem xpsring1d

Description: The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025)

Ref Expression
Hypotheses xpsringd.y 
|- Y = ( S Xs. R )
xpsringd.s 
|- ( ph -> S e. Ring )
xpsringd.r 
|- ( ph -> R e. Ring )
Assertion xpsring1d 
|- ( ph -> ( 1r ` Y ) = <. ( 1r ` S ) , ( 1r ` R ) >. )

Proof

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