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 syl5eq
 |-  ( ( 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. ) )