Metamath Proof Explorer

Theorem prdsinvlem

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

Ref Expression
Hypotheses prdsinvlem.y 
|- Y = ( S Xs_ R )
prdsinvlem.b 
|- B = ( Base ` Y )
prdsinvlem.p 
|- .+ = ( +g ` Y )
prdsinvlem.s 
|- ( ph -> S e. V )
prdsinvlem.i 
|- ( ph -> I e. W )
prdsinvlem.r 
|- ( ph -> R : I --> Grp )
prdsinvlem.f 
|- ( ph -> F e. B )
prdsinvlem.z 
|- .0. = ( 0g o. R )
prdsinvlem.n 
|- N = ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) )
Assertion prdsinvlem 
|- ( ph -> ( N e. B /\ ( N .+ F ) = .0. ) )

Proof

Step Hyp Ref Expression
1 prdsinvlem.y 
 |-  Y = ( S Xs_ R )
2 prdsinvlem.b 
 |-  B = ( Base ` Y )
3 prdsinvlem.p 
 |-  .+ = ( +g ` Y )
4 prdsinvlem.s 
 |-  ( ph -> S e. V )
5 prdsinvlem.i 
 |-  ( ph -> I e. W )
6 prdsinvlem.r 
 |-  ( ph -> R : I --> Grp )
7 prdsinvlem.f 
 |-  ( ph -> F e. B )
8 prdsinvlem.z 
 |-  .0. = ( 0g o. R )
9 prdsinvlem.n 
 |-  N = ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) )
10 6 ffvelrnda 
 |-  ( ( ph /\ y e. I ) -> ( R ` y ) e. Grp )
11 4 adantr 
 |-  ( ( ph /\ y e. I ) -> S e. V )
12 5 adantr 
 |-  ( ( ph /\ y e. I ) -> I e. W )
13 6 ffnd 
 |-  ( ph -> R Fn I )
14 13 adantr 
 |-  ( ( ph /\ y e. I ) -> R Fn I )
15 7 adantr 
 |-  ( ( ph /\ y e. I ) -> F e. B )
16 simpr 
 |-  ( ( ph /\ y e. I ) -> y e. I )
17 1 2 11 12 14 15 16 prdsbasprj 
 |-  ( ( ph /\ y e. I ) -> ( F ` y ) e. ( Base ` ( R ` y ) ) )
18 eqid 
 |-  ( Base ` ( R ` y ) ) = ( Base ` ( R ` y ) )
19 eqid 
 |-  ( invg ` ( R ` y ) ) = ( invg ` ( R ` y ) )
20 18 19 grpinvcl 
 |-  ( ( ( R ` y ) e. Grp /\ ( F ` y ) e. ( Base ` ( R ` y ) ) ) -> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) e. ( Base ` ( R ` y ) ) )
21 10 17 20 syl2anc 
 |-  ( ( ph /\ y e. I ) -> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) e. ( Base ` ( R ` y ) ) )
22 21 ralrimiva 
 |-  ( ph -> A. y e. I ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) e. ( Base ` ( R ` y ) ) )
23 1 2 4 5 13 prdsbasmpt 
 |-  ( ph -> ( ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) ) e. B <-> A. y e. I ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) e. ( Base ` ( R ` y ) ) ) )
24 22 23 mpbird 
 |-  ( ph -> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) ) e. B )
25 9 24 eqeltrid 
 |-  ( ph -> N e. B )
26 6 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. Grp )
27 4 adantr 
 |-  ( ( ph /\ x e. I ) -> S e. V )
28 5 adantr 
 |-  ( ( ph /\ x e. I ) -> I e. W )
29 13 adantr 
 |-  ( ( ph /\ x e. I ) -> R Fn I )
30 7 adantr 
 |-  ( ( ph /\ x e. I ) -> F e. B )
31 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
32 1 2 27 28 29 30 31 prdsbasprj 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. ( Base ` ( R ` x ) ) )
33 eqid 
 |-  ( Base ` ( R ` x ) ) = ( Base ` ( R ` x ) )
34 eqid 
 |-  ( +g ` ( R ` x ) ) = ( +g ` ( R ` x ) )
35 eqid 
 |-  ( 0g ` ( R ` x ) ) = ( 0g ` ( R ` x ) )
36 eqid 
 |-  ( invg ` ( R ` x ) ) = ( invg ` ( R ` x ) )
37 33 34 35 36 grplinv 
 |-  ( ( ( R ` x ) e. Grp /\ ( F ` x ) e. ( Base ` ( R ` x ) ) ) -> ( ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) ( +g ` ( R ` x ) ) ( F ` x ) ) = ( 0g ` ( R ` x ) ) )
38 26 32 37 syl2anc 
 |-  ( ( ph /\ x e. I ) -> ( ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) ( +g ` ( R ` x ) ) ( F ` x ) ) = ( 0g ` ( R ` x ) ) )
39 2fveq3 
 |-  ( y = x -> ( invg ` ( R ` y ) ) = ( invg ` ( R ` x ) ) )
40 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
41 39 40 fveq12d 
 |-  ( y = x -> ( ( invg ` ( R ` y ) ) ` ( F ` y ) ) = ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) )
42 fvex 
 |-  ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) e. _V
43 41 9 42 fvmpt 
 |-  ( x e. I -> ( N ` x ) = ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) )
44 43 adantl 
 |-  ( ( ph /\ x e. I ) -> ( N ` x ) = ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) )
45 44 oveq1d 
 |-  ( ( ph /\ x e. I ) -> ( ( N ` x ) ( +g ` ( R ` x ) ) ( F ` x ) ) = ( ( ( invg ` ( R ` x ) ) ` ( F ` x ) ) ( +g ` ( R ` x ) ) ( F ` x ) ) )
46 8 fveq1i 
 |-  ( .0. ` x ) = ( ( 0g o. R ) ` x )
47 fvco2 
 |-  ( ( R Fn I /\ x e. I ) -> ( ( 0g o. R ) ` x ) = ( 0g ` ( R ` x ) ) )
48 13 47 sylan 
 |-  ( ( ph /\ x e. I ) -> ( ( 0g o. R ) ` x ) = ( 0g ` ( R ` x ) ) )
49 46 48 eqtrid 
 |-  ( ( ph /\ x e. I ) -> ( .0. ` x ) = ( 0g ` ( R ` x ) ) )
50 38 45 49 3eqtr4d 
 |-  ( ( ph /\ x e. I ) -> ( ( N ` x ) ( +g ` ( R ` x ) ) ( F ` x ) ) = ( .0. ` x ) )
51 50 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( ( N ` x ) ( +g ` ( R ` x ) ) ( F ` x ) ) ) = ( x e. I |-> ( .0. ` x ) ) )
52 1 2 4 5 13 25 7 3 prdsplusgval 
 |-  ( ph -> ( N .+ F ) = ( x e. I |-> ( ( N ` x ) ( +g ` ( R ` x ) ) ( F ` x ) ) ) )
53 fn0g 
 |-  0g Fn _V
54 ssv 
 |-  ran R C_ _V
55 54 a1i 
 |-  ( ph -> ran R C_ _V )
56 fnco 
 |-  ( ( 0g Fn _V /\ R Fn I /\ ran R C_ _V ) -> ( 0g o. R ) Fn I )
57 53 13 55 56 mp3an2i 
 |-  ( ph -> ( 0g o. R ) Fn I )
58 8 fneq1i 
 |-  ( .0. Fn I <-> ( 0g o. R ) Fn I )
59 57 58 sylibr 
 |-  ( ph -> .0. Fn I )
60 dffn5 
 |-  ( .0. Fn I <-> .0. = ( x e. I |-> ( .0. ` x ) ) )
61 59 60 sylib 
 |-  ( ph -> .0. = ( x e. I |-> ( .0. ` x ) ) )
62 51 52 61 3eqtr4d 
 |-  ( ph -> ( N .+ F ) = .0. )
63 25 62 jca 
 |-  ( ph -> ( N e. B /\ ( N .+ F ) = .0. ) )