Step |
Hyp |
Ref |
Expression |
1 |
|
dprdf1o.1 |
|- ( ph -> G dom DProd S ) |
2 |
|
dprdf1o.2 |
|- ( ph -> dom S = I ) |
3 |
|
dprdf1o.3 |
|- ( ph -> F : J -1-1-onto-> I ) |
4 |
|
eqid |
|- ( Cntz ` G ) = ( Cntz ` G ) |
5 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
6 |
|
eqid |
|- ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) ) |
7 |
|
dprdgrp |
|- ( G dom DProd S -> G e. Grp ) |
8 |
1 7
|
syl |
|- ( ph -> G e. Grp ) |
9 |
|
f1of1 |
|- ( F : J -1-1-onto-> I -> F : J -1-1-> I ) |
10 |
3 9
|
syl |
|- ( ph -> F : J -1-1-> I ) |
11 |
1 2
|
dprddomcld |
|- ( ph -> I e. _V ) |
12 |
|
f1dmex |
|- ( ( F : J -1-1-> I /\ I e. _V ) -> J e. _V ) |
13 |
10 11 12
|
syl2anc |
|- ( ph -> J e. _V ) |
14 |
1 2
|
dprdf2 |
|- ( ph -> S : I --> ( SubGrp ` G ) ) |
15 |
|
f1of |
|- ( F : J -1-1-onto-> I -> F : J --> I ) |
16 |
3 15
|
syl |
|- ( ph -> F : J --> I ) |
17 |
|
fco |
|- ( ( S : I --> ( SubGrp ` G ) /\ F : J --> I ) -> ( S o. F ) : J --> ( SubGrp ` G ) ) |
18 |
14 16 17
|
syl2anc |
|- ( ph -> ( S o. F ) : J --> ( SubGrp ` G ) ) |
19 |
1
|
adantr |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> G dom DProd S ) |
20 |
2
|
adantr |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> dom S = I ) |
21 |
16
|
adantr |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> F : J --> I ) |
22 |
|
simpr1 |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> x e. J ) |
23 |
21 22
|
ffvelrnd |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( F ` x ) e. I ) |
24 |
|
simpr2 |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> y e. J ) |
25 |
21 24
|
ffvelrnd |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( F ` y ) e. I ) |
26 |
|
simpr3 |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> x =/= y ) |
27 |
10
|
adantr |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> F : J -1-1-> I ) |
28 |
|
f1fveq |
|- ( ( F : J -1-1-> I /\ ( x e. J /\ y e. J ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) ) |
29 |
27 22 24 28
|
syl12anc |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) ) |
30 |
29
|
necon3bid |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( F ` x ) =/= ( F ` y ) <-> x =/= y ) ) |
31 |
26 30
|
mpbird |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( F ` x ) =/= ( F ` y ) ) |
32 |
19 20 23 25 31 4
|
dprdcntz |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( S ` ( F ` x ) ) C_ ( ( Cntz ` G ) ` ( S ` ( F ` y ) ) ) ) |
33 |
|
fvco3 |
|- ( ( F : J --> I /\ x e. J ) -> ( ( S o. F ) ` x ) = ( S ` ( F ` x ) ) ) |
34 |
21 22 33
|
syl2anc |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( S o. F ) ` x ) = ( S ` ( F ` x ) ) ) |
35 |
|
fvco3 |
|- ( ( F : J --> I /\ y e. J ) -> ( ( S o. F ) ` y ) = ( S ` ( F ` y ) ) ) |
36 |
21 24 35
|
syl2anc |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( S o. F ) ` y ) = ( S ` ( F ` y ) ) ) |
37 |
36
|
fveq2d |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( Cntz ` G ) ` ( ( S o. F ) ` y ) ) = ( ( Cntz ` G ) ` ( S ` ( F ` y ) ) ) ) |
38 |
32 34 37
|
3sstr4d |
|- ( ( ph /\ ( x e. J /\ y e. J /\ x =/= y ) ) -> ( ( S o. F ) ` x ) C_ ( ( Cntz ` G ) ` ( ( S o. F ) ` y ) ) ) |
39 |
16 33
|
sylan |
|- ( ( ph /\ x e. J ) -> ( ( S o. F ) ` x ) = ( S ` ( F ` x ) ) ) |
40 |
|
imaco |
|- ( ( S o. F ) " ( J \ { x } ) ) = ( S " ( F " ( J \ { x } ) ) ) |
41 |
3
|
adantr |
|- ( ( ph /\ x e. J ) -> F : J -1-1-onto-> I ) |
42 |
|
dff1o3 |
|- ( F : J -1-1-onto-> I <-> ( F : J -onto-> I /\ Fun `' F ) ) |
43 |
42
|
simprbi |
|- ( F : J -1-1-onto-> I -> Fun `' F ) |
44 |
|
imadif |
|- ( Fun `' F -> ( F " ( J \ { x } ) ) = ( ( F " J ) \ ( F " { x } ) ) ) |
45 |
41 43 44
|
3syl |
|- ( ( ph /\ x e. J ) -> ( F " ( J \ { x } ) ) = ( ( F " J ) \ ( F " { x } ) ) ) |
46 |
|
f1ofo |
|- ( F : J -1-1-onto-> I -> F : J -onto-> I ) |
47 |
|
foima |
|- ( F : J -onto-> I -> ( F " J ) = I ) |
48 |
41 46 47
|
3syl |
|- ( ( ph /\ x e. J ) -> ( F " J ) = I ) |
49 |
|
f1ofn |
|- ( F : J -1-1-onto-> I -> F Fn J ) |
50 |
3 49
|
syl |
|- ( ph -> F Fn J ) |
51 |
|
fnsnfv |
|- ( ( F Fn J /\ x e. J ) -> { ( F ` x ) } = ( F " { x } ) ) |
52 |
50 51
|
sylan |
|- ( ( ph /\ x e. J ) -> { ( F ` x ) } = ( F " { x } ) ) |
53 |
52
|
eqcomd |
|- ( ( ph /\ x e. J ) -> ( F " { x } ) = { ( F ` x ) } ) |
54 |
48 53
|
difeq12d |
|- ( ( ph /\ x e. J ) -> ( ( F " J ) \ ( F " { x } ) ) = ( I \ { ( F ` x ) } ) ) |
55 |
45 54
|
eqtrd |
|- ( ( ph /\ x e. J ) -> ( F " ( J \ { x } ) ) = ( I \ { ( F ` x ) } ) ) |
56 |
55
|
imaeq2d |
|- ( ( ph /\ x e. J ) -> ( S " ( F " ( J \ { x } ) ) ) = ( S " ( I \ { ( F ` x ) } ) ) ) |
57 |
40 56
|
syl5eq |
|- ( ( ph /\ x e. J ) -> ( ( S o. F ) " ( J \ { x } ) ) = ( S " ( I \ { ( F ` x ) } ) ) ) |
58 |
57
|
unieqd |
|- ( ( ph /\ x e. J ) -> U. ( ( S o. F ) " ( J \ { x } ) ) = U. ( S " ( I \ { ( F ` x ) } ) ) ) |
59 |
58
|
fveq2d |
|- ( ( ph /\ x e. J ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { ( F ` x ) } ) ) ) ) |
60 |
39 59
|
ineq12d |
|- ( ( ph /\ x e. J ) -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) = ( ( S ` ( F ` x ) ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { ( F ` x ) } ) ) ) ) ) |
61 |
1
|
adantr |
|- ( ( ph /\ x e. J ) -> G dom DProd S ) |
62 |
2
|
adantr |
|- ( ( ph /\ x e. J ) -> dom S = I ) |
63 |
16
|
ffvelrnda |
|- ( ( ph /\ x e. J ) -> ( F ` x ) e. I ) |
64 |
61 62 63 5 6
|
dprddisj |
|- ( ( ph /\ x e. J ) -> ( ( S ` ( F ` x ) ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( I \ { ( F ` x ) } ) ) ) ) = { ( 0g ` G ) } ) |
65 |
60 64
|
eqtrd |
|- ( ( ph /\ x e. J ) -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) = { ( 0g ` G ) } ) |
66 |
|
eqimss |
|- ( ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) = { ( 0g ` G ) } -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) C_ { ( 0g ` G ) } ) |
67 |
65 66
|
syl |
|- ( ( ph /\ x e. J ) -> ( ( ( S o. F ) ` x ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( ( S o. F ) " ( J \ { x } ) ) ) ) C_ { ( 0g ` G ) } ) |
68 |
4 5 6 8 13 18 38 67
|
dmdprdd |
|- ( ph -> G dom DProd ( S o. F ) ) |
69 |
|
rnco2 |
|- ran ( S o. F ) = ( S " ran F ) |
70 |
|
forn |
|- ( F : J -onto-> I -> ran F = I ) |
71 |
3 46 70
|
3syl |
|- ( ph -> ran F = I ) |
72 |
71
|
imaeq2d |
|- ( ph -> ( S " ran F ) = ( S " I ) ) |
73 |
|
ffn |
|- ( S : I --> ( SubGrp ` G ) -> S Fn I ) |
74 |
|
fnima |
|- ( S Fn I -> ( S " I ) = ran S ) |
75 |
14 73 74
|
3syl |
|- ( ph -> ( S " I ) = ran S ) |
76 |
72 75
|
eqtrd |
|- ( ph -> ( S " ran F ) = ran S ) |
77 |
69 76
|
syl5eq |
|- ( ph -> ran ( S o. F ) = ran S ) |
78 |
77
|
unieqd |
|- ( ph -> U. ran ( S o. F ) = U. ran S ) |
79 |
78
|
fveq2d |
|- ( ph -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S o. F ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
80 |
6
|
dprdspan |
|- ( G dom DProd ( S o. F ) -> ( G DProd ( S o. F ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S o. F ) ) ) |
81 |
68 80
|
syl |
|- ( ph -> ( G DProd ( S o. F ) ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran ( S o. F ) ) ) |
82 |
6
|
dprdspan |
|- ( G dom DProd S -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
83 |
1 82
|
syl |
|- ( ph -> ( G DProd S ) = ( ( mrCls ` ( SubGrp ` G ) ) ` U. ran S ) ) |
84 |
79 81 83
|
3eqtr4d |
|- ( ph -> ( G DProd ( S o. F ) ) = ( G DProd S ) ) |
85 |
68 84
|
jca |
|- ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) = ( G DProd S ) ) ) |