Step |
Hyp |
Ref |
Expression |
1 |
|
elpi1.g |
|- G = ( J pi1 Y ) |
2 |
|
elpi1.b |
|- B = ( Base ` G ) |
3 |
|
elpi1.1 |
|- ( ph -> J e. ( TopOn ` X ) ) |
4 |
|
elpi1.2 |
|- ( ph -> Y e. X ) |
5 |
|
pi1addf.p |
|- .+ = ( +g ` G ) |
6 |
|
eqidd |
|- ( ph -> ( ( J Om1 Y ) /s ( ~=ph ` J ) ) = ( ( J Om1 Y ) /s ( ~=ph ` J ) ) ) |
7 |
|
eqidd |
|- ( ph -> ( Base ` ( J Om1 Y ) ) = ( Base ` ( J Om1 Y ) ) ) |
8 |
|
fvexd |
|- ( ph -> ( ~=ph ` J ) e. _V ) |
9 |
|
ovexd |
|- ( ph -> ( J Om1 Y ) e. _V ) |
10 |
|
eqid |
|- ( J Om1 Y ) = ( J Om1 Y ) |
11 |
2
|
a1i |
|- ( ph -> B = ( Base ` G ) ) |
12 |
1 3 4 10 11 7
|
pi1blem |
|- ( ph -> ( ( ( ~=ph ` J ) " ( Base ` ( J Om1 Y ) ) ) C_ ( Base ` ( J Om1 Y ) ) /\ ( Base ` ( J Om1 Y ) ) C_ ( II Cn J ) ) ) |
13 |
12
|
simpld |
|- ( ph -> ( ( ~=ph ` J ) " ( Base ` ( J Om1 Y ) ) ) C_ ( Base ` ( J Om1 Y ) ) ) |
14 |
6 7 8 9 13
|
qusin |
|- ( ph -> ( ( J Om1 Y ) /s ( ~=ph ` J ) ) = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) ) ) |
15 |
1 3 4 10
|
pi1val |
|- ( ph -> G = ( ( J Om1 Y ) /s ( ~=ph ` J ) ) ) |
16 |
1 3 4 10 11 7
|
pi1buni |
|- ( ph -> U. B = ( Base ` ( J Om1 Y ) ) ) |
17 |
16
|
sqxpeqd |
|- ( ph -> ( U. B X. U. B ) = ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) |
18 |
17
|
ineq2d |
|- ( ph -> ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( ( ~=ph ` J ) i^i ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) ) |
19 |
18
|
oveq2d |
|- ( ph -> ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( ( Base ` ( J Om1 Y ) ) X. ( Base ` ( J Om1 Y ) ) ) ) ) ) |
20 |
14 15 19
|
3eqtr4d |
|- ( ph -> G = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) |
21 |
|
phtpcer |
|- ( ~=ph ` J ) Er ( II Cn J ) |
22 |
21
|
a1i |
|- ( ph -> ( ~=ph ` J ) Er ( II Cn J ) ) |
23 |
12
|
simprd |
|- ( ph -> ( Base ` ( J Om1 Y ) ) C_ ( II Cn J ) ) |
24 |
16 23
|
eqsstrd |
|- ( ph -> U. B C_ ( II Cn J ) ) |
25 |
22 24
|
erinxp |
|- ( ph -> ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) Er U. B ) |
26 |
|
eqid |
|- ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) |
27 |
|
eqid |
|- ( +g ` ( J Om1 Y ) ) = ( +g ` ( J Om1 Y ) ) |
28 |
1 3 4 11 26 10 27
|
pi1cpbl |
|- ( ph -> ( ( a ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) c /\ b ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) d ) -> ( a ( +g ` ( J Om1 Y ) ) b ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( c ( +g ` ( J Om1 Y ) ) d ) ) ) |
29 |
3
|
adantr |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> J e. ( TopOn ` X ) ) |
30 |
4
|
adantr |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> Y e. X ) |
31 |
10 29 30
|
om1plusg |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( *p ` J ) = ( +g ` ( J Om1 Y ) ) ) |
32 |
31
|
oveqd |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( c ( *p ` J ) d ) = ( c ( +g ` ( J Om1 Y ) ) d ) ) |
33 |
16
|
adantr |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> U. B = ( Base ` ( J Om1 Y ) ) ) |
34 |
|
simprl |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> c e. U. B ) |
35 |
|
simprr |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> d e. U. B ) |
36 |
10 29 30 33 34 35
|
om1addcl |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( c ( *p ` J ) d ) e. U. B ) |
37 |
32 36
|
eqeltrrd |
|- ( ( ph /\ ( c e. U. B /\ d e. U. B ) ) -> ( c ( +g ` ( J Om1 Y ) ) d ) e. U. B ) |
38 |
20 16 25 9 28 37 27 5
|
qusaddf |
|- ( ph -> .+ : ( ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) X. ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) --> ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) |
39 |
1 3 4 11 26
|
pi1bas3 |
|- ( ph -> B = ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) |
40 |
39
|
sqxpeqd |
|- ( ph -> ( B X. B ) = ( ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) X. ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) ) |
41 |
40
|
feq2d |
|- ( ph -> ( .+ : ( B X. B ) --> ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) <-> .+ : ( ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) X. ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) --> ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) ) |
42 |
38 41
|
mpbird |
|- ( ph -> .+ : ( B X. B ) --> ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) |
43 |
39
|
feq3d |
|- ( ph -> ( .+ : ( B X. B ) --> B <-> .+ : ( B X. B ) --> ( U. B /. ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) ) ) |
44 |
42 43
|
mpbird |
|- ( ph -> .+ : ( B X. B ) --> B ) |