This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prds0g

Description: The identity in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsmndd.y 
|- Y = ( S Xs_ R )
prdsmndd.i 
|- ( ph -> I e. W )
prdsmndd.s 
|- ( ph -> S e. V )
prdsmndd.r 
|- ( ph -> R : I --> Mnd )
Assertion prds0g 
|- ( ph -> ( 0g o. R ) = ( 0g ` Y ) )

Proof

Step Hyp Ref Expression
1 prdsmndd.y 
 |-  Y = ( S Xs_ R )
2 prdsmndd.i 
 |-  ( ph -> I e. W )
3 prdsmndd.s 
 |-  ( ph -> S e. V )
4 prdsmndd.r 
 |-  ( ph -> R : I --> Mnd )
5 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
6 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
7 3 elexd 
 |-  ( ph -> S e. _V )
8 2 elexd 
 |-  ( ph -> I e. _V )
9 eqid 
 |-  ( 0g o. R ) = ( 0g o. R )
10 1 5 6 7 8 4 9 prdsidlem 
 |-  ( ph -> ( ( 0g o. R ) e. ( Base ` Y ) /\ A. b e. ( Base ` Y ) ( ( ( 0g o. R ) ( +g ` Y ) b ) = b /\ ( b ( +g ` Y ) ( 0g o. R ) ) = b ) ) )
11 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
12 1 2 3 4 prdsmndd 
 |-  ( ph -> Y e. Mnd )
13 5 6 mndid 
 |-  ( Y e. Mnd -> E. a e. ( Base ` Y ) A. b e. ( Base ` Y ) ( ( a ( +g ` Y ) b ) = b /\ ( b ( +g ` Y ) a ) = b ) )
14 12 13 syl 
 |-  ( ph -> E. a e. ( Base ` Y ) A. b e. ( Base ` Y ) ( ( a ( +g ` Y ) b ) = b /\ ( b ( +g ` Y ) a ) = b ) )
15 5 11 6 14 ismgmid 
 |-  ( ph -> ( ( ( 0g o. R ) e. ( Base ` Y ) /\ A. b e. ( Base ` Y ) ( ( ( 0g o. R ) ( +g ` Y ) b ) = b /\ ( b ( +g ` Y ) ( 0g o. R ) ) = b ) ) <-> ( 0g ` Y ) = ( 0g o. R ) ) )
16 10 15 mpbid 
 |-  ( ph -> ( 0g ` Y ) = ( 0g o. R ) )
17 16 eqcomd 
 |-  ( ph -> ( 0g o. R ) = ( 0g ` Y ) )