Metamath Proof Explorer


Theorem pi1addf

Description: The group operation of pi1 is a binary operation. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses elpi1.g
|- G = ( J pi1 Y )
elpi1.b
|- B = ( Base ` G )
elpi1.1
|- ( ph -> J e. ( TopOn ` X ) )
elpi1.2
|- ( ph -> Y e. X )
pi1addf.p
|- .+ = ( +g ` G )
Assertion pi1addf
|- ( ph -> .+ : ( B X. B ) --> B )

Proof

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 )