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