Metamath Proof Explorer

Theorem prdsidlem

Description: Characterization of identity in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses prdsplusgcl.y 
|- Y = ( S Xs_ R )
prdsplusgcl.b 
|- B = ( Base ` Y )
prdsplusgcl.p 
|- .+ = ( +g ` Y )
prdsplusgcl.s 
|- ( ph -> S e. V )
prdsplusgcl.i 
|- ( ph -> I e. W )
prdsplusgcl.r 
|- ( ph -> R : I --> Mnd )
prdsidlem.z 
|- .0. = ( 0g o. R )
Assertion prdsidlem 
|- ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )

Proof

Step Hyp Ref Expression
1 prdsplusgcl.y 
 |-  Y = ( S Xs_ R )
2 prdsplusgcl.b 
 |-  B = ( Base ` Y )
3 prdsplusgcl.p 
 |-  .+ = ( +g ` Y )
4 prdsplusgcl.s 
 |-  ( ph -> S e. V )
5 prdsplusgcl.i 
 |-  ( ph -> I e. W )
6 prdsplusgcl.r 
 |-  ( ph -> R : I --> Mnd )
7 prdsidlem.z 
 |-  .0. = ( 0g o. R )
8 fvexd 
 |-  ( ( ph /\ y e. I ) -> ( R ` y ) e. _V )
9 6 feqmptd 
 |-  ( ph -> R = ( y e. I |-> ( R ` y ) ) )
10 fn0g 
 |-  0g Fn _V
11 10 a1i 
 |-  ( ph -> 0g Fn _V )
12 dffn5 
 |-  ( 0g Fn _V <-> 0g = ( x e. _V |-> ( 0g ` x ) ) )
13 11 12 sylib 
 |-  ( ph -> 0g = ( x e. _V |-> ( 0g ` x ) ) )
14 fveq2 
 |-  ( x = ( R ` y ) -> ( 0g ` x ) = ( 0g ` ( R ` y ) ) )
15 8 9 13 14 fmptco 
 |-  ( ph -> ( 0g o. R ) = ( y e. I |-> ( 0g ` ( R ` y ) ) ) )
16 7 15 syl5eq 
 |-  ( ph -> .0. = ( y e. I |-> ( 0g ` ( R ` y ) ) ) )
17 6 ffvelrnda 
 |-  ( ( ph /\ y e. I ) -> ( R ` y ) e. Mnd )
18 eqid 
 |-  ( Base ` ( R ` y ) ) = ( Base ` ( R ` y ) )
19 eqid 
 |-  ( 0g ` ( R ` y ) ) = ( 0g ` ( R ` y ) )
20 18 19 mndidcl 
 |-  ( ( R ` y ) e. Mnd -> ( 0g ` ( R ` y ) ) e. ( Base ` ( R ` y ) ) )
21 17 20 syl 
 |-  ( ( ph /\ y e. I ) -> ( 0g ` ( R ` y ) ) e. ( Base ` ( R ` y ) ) )
22 21 ralrimiva 
 |-  ( ph -> A. y e. I ( 0g ` ( R ` y ) ) e. ( Base ` ( R ` y ) ) )
23 6 ffnd 
 |-  ( ph -> R Fn I )
24 1 2 4 5 23 prdsbasmpt 
 |-  ( ph -> ( ( y e. I |-> ( 0g ` ( R ` y ) ) ) e. B <-> A. y e. I ( 0g ` ( R ` y ) ) e. ( Base ` ( R ` y ) ) ) )
25 22 24 mpbird 
 |-  ( ph -> ( y e. I |-> ( 0g ` ( R ` y ) ) ) e. B )
26 16 25 eqeltrd 
 |-  ( ph -> .0. e. B )
27 7 fveq1i 
 |-  ( .0. ` y ) = ( ( 0g o. R ) ` y )
28 fvco2 
 |-  ( ( R Fn I /\ y e. I ) -> ( ( 0g o. R ) ` y ) = ( 0g ` ( R ` y ) ) )
29 23 28 sylan 
 |-  ( ( ph /\ y e. I ) -> ( ( 0g o. R ) ` y ) = ( 0g ` ( R ` y ) ) )
30 27 29 syl5eq 
 |-  ( ( ph /\ y e. I ) -> ( .0. ` y ) = ( 0g ` ( R ` y ) ) )
31 30 adantlr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( .0. ` y ) = ( 0g ` ( R ` y ) ) )
32 31 oveq1d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( ( .0. ` y ) ( +g ` ( R ` y ) ) ( x ` y ) ) = ( ( 0g ` ( R ` y ) ) ( +g ` ( R ` y ) ) ( x ` y ) ) )
33 6 adantr 
 |-  ( ( ph /\ x e. B ) -> R : I --> Mnd )
34 33 ffvelrnda 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( R ` y ) e. Mnd )
35 4 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> S e. V )
36 5 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> I e. W )
37 23 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> R Fn I )
38 simplr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> x e. B )
39 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> y e. I )
40 1 2 35 36 37 38 39 prdsbasprj 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( x ` y ) e. ( Base ` ( R ` y ) ) )
41 eqid 
 |-  ( +g ` ( R ` y ) ) = ( +g ` ( R ` y ) )
42 18 41 19 mndlid 
 |-  ( ( ( R ` y ) e. Mnd /\ ( x ` y ) e. ( Base ` ( R ` y ) ) ) -> ( ( 0g ` ( R ` y ) ) ( +g ` ( R ` y ) ) ( x ` y ) ) = ( x ` y ) )
43 34 40 42 syl2anc 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( ( 0g ` ( R ` y ) ) ( +g ` ( R ` y ) ) ( x ` y ) ) = ( x ` y ) )
44 32 43 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( ( .0. ` y ) ( +g ` ( R ` y ) ) ( x ` y ) ) = ( x ` y ) )
45 44 mpteq2dva 
 |-  ( ( ph /\ x e. B ) -> ( y e. I |-> ( ( .0. ` y ) ( +g ` ( R ` y ) ) ( x ` y ) ) ) = ( y e. I |-> ( x ` y ) ) )
46 4 adantr 
 |-  ( ( ph /\ x e. B ) -> S e. V )
47 5 adantr 
 |-  ( ( ph /\ x e. B ) -> I e. W )
48 23 adantr 
 |-  ( ( ph /\ x e. B ) -> R Fn I )
49 26 adantr 
 |-  ( ( ph /\ x e. B ) -> .0. e. B )
50 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
51 1 2 46 47 48 49 50 3 prdsplusgval 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = ( y e. I |-> ( ( .0. ` y ) ( +g ` ( R ` y ) ) ( x ` y ) ) ) )
52 1 2 46 47 48 50 prdsbasfn 
 |-  ( ( ph /\ x e. B ) -> x Fn I )
53 dffn5 
 |-  ( x Fn I <-> x = ( y e. I |-> ( x ` y ) ) )
54 52 53 sylib 
 |-  ( ( ph /\ x e. B ) -> x = ( y e. I |-> ( x ` y ) ) )
55 45 51 54 3eqtr4d 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
56 31 oveq2d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( ( x ` y ) ( +g ` ( R ` y ) ) ( .0. ` y ) ) = ( ( x ` y ) ( +g ` ( R ` y ) ) ( 0g ` ( R ` y ) ) ) )
57 18 41 19 mndrid 
 |-  ( ( ( R ` y ) e. Mnd /\ ( x ` y ) e. ( Base ` ( R ` y ) ) ) -> ( ( x ` y ) ( +g ` ( R ` y ) ) ( 0g ` ( R ` y ) ) ) = ( x ` y ) )
58 34 40 57 syl2anc 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( ( x ` y ) ( +g ` ( R ` y ) ) ( 0g ` ( R ` y ) ) ) = ( x ` y ) )
59 56 58 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. I ) -> ( ( x ` y ) ( +g ` ( R ` y ) ) ( .0. ` y ) ) = ( x ` y ) )
60 59 mpteq2dva 
 |-  ( ( ph /\ x e. B ) -> ( y e. I |-> ( ( x ` y ) ( +g ` ( R ` y ) ) ( .0. ` y ) ) ) = ( y e. I |-> ( x ` y ) ) )
61 1 2 46 47 48 50 49 3 prdsplusgval 
 |-  ( ( ph /\ x e. B ) -> ( x .+ .0. ) = ( y e. I |-> ( ( x ` y ) ( +g ` ( R ` y ) ) ( .0. ` y ) ) ) )
62 60 61 54 3eqtr4d 
 |-  ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
63 55 62 jca 
 |-  ( ( ph /\ x e. B ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
64 63 ralrimiva 
 |-  ( ph -> A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
65 26 64 jca 
 |-  ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )