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 )