Metamath Proof Explorer

Theorem sitgaddlemb

Description: Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019)

Ref Expression
Hypotheses sitgval.b 
|- B = ( Base ` W )
sitgval.j 
|- J = ( TopOpen ` W )
sitgval.s 
|- S = ( sigaGen ` J )
sitgval.0 
|- .0. = ( 0g ` W )
sitgval.x 
|- .x. = ( .s ` W )
sitgval.h 
|- H = ( RRHom ` ( Scalar ` W ) )
sitgval.1 
|- ( ph -> W e. V )
sitgval.2 
|- ( ph -> M e. U. ran measures )
sitgadd.1 
|- ( ph -> W e. TopSp )
sitgadd.2 
|- ( ph -> ( W |`v ( H " ( 0 [,) +oo ) ) ) e. SLMod )
sitgadd.3 
|- ( ph -> J e. Fre )
sitgadd.4 
|- ( ph -> F e. dom ( W sitg M ) )
sitgadd.5 
|- ( ph -> G e. dom ( W sitg M ) )
sitgadd.6 
|- ( ph -> ( Scalar ` W ) e. RRExt )
sitgadd.7 
|- .+ = ( +g ` W )
Assertion sitgaddlemb 
|- ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) .x. ( 2nd ` p ) ) e. B )

Proof

Step Hyp Ref Expression
1 sitgval.b 
 |-  B = ( Base ` W )
2 sitgval.j 
 |-  J = ( TopOpen ` W )
3 sitgval.s 
 |-  S = ( sigaGen ` J )
4 sitgval.0 
 |-  .0. = ( 0g ` W )
5 sitgval.x 
 |-  .x. = ( .s ` W )
6 sitgval.h 
 |-  H = ( RRHom ` ( Scalar ` W ) )
7 sitgval.1 
 |-  ( ph -> W e. V )
8 sitgval.2 
 |-  ( ph -> M e. U. ran measures )
9 sitgadd.1 
 |-  ( ph -> W e. TopSp )
10 sitgadd.2 
 |-  ( ph -> ( W |`v ( H " ( 0 [,) +oo ) ) ) e. SLMod )
11 sitgadd.3 
 |-  ( ph -> J e. Fre )
12 sitgadd.4 
 |-  ( ph -> F e. dom ( W sitg M ) )
13 sitgadd.5 
 |-  ( ph -> G e. dom ( W sitg M ) )
14 sitgadd.6 
 |-  ( ph -> ( Scalar ` W ) e. RRExt )
15 sitgadd.7 
 |-  .+ = ( +g ` W )
16 10 adantr 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( W |`v ( H " ( 0 [,) +oo ) ) ) e. SLMod )
17 simpl 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ph )
18 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
19 18 rrhfe 
 |-  ( ( Scalar ` W ) e. RRExt -> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
20 14 19 syl 
 |-  ( ph -> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
21 6 feq1i 
 |-  ( H : RR --> ( Base ` ( Scalar ` W ) ) <-> ( RRHom ` ( Scalar ` W ) ) : RR --> ( Base ` ( Scalar ` W ) ) )
22 20 21 sylibr 
 |-  ( ph -> H : RR --> ( Base ` ( Scalar ` W ) ) )
23 22 ffnd 
 |-  ( ph -> H Fn RR )
24 17 23 syl 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> H Fn RR )
25 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
26 25 a1i 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( 0 [,) +oo ) C_ RR )
27 simpr 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) )
28 27 eldifad 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> p e. ( ran F X. ran G ) )
29 xp1st 
 |-  ( p e. ( ran F X. ran G ) -> ( 1st ` p ) e. ran F )
30 28 29 syl 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( 1st ` p ) e. ran F )
31 xp2nd 
 |-  ( p e. ( ran F X. ran G ) -> ( 2nd ` p ) e. ran G )
32 28 31 syl 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( 2nd ` p ) e. ran G )
33 27 eldifbd 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> -. p e. { <. .0. , .0. >. } )
34 velsn 
 |-  ( p e. { <. .0. , .0. >. } <-> p = <. .0. , .0. >. )
35 34 notbii 
 |-  ( -. p e. { <. .0. , .0. >. } <-> -. p = <. .0. , .0. >. )
36 33 35 sylib 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> -. p = <. .0. , .0. >. )
37 eqopi 
 |-  ( ( p e. ( ran F X. ran G ) /\ ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) ) -> p = <. .0. , .0. >. )
38 37 ex 
 |-  ( p e. ( ran F X. ran G ) -> ( ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) -> p = <. .0. , .0. >. ) )
39 38 con3d 
 |-  ( p e. ( ran F X. ran G ) -> ( -. p = <. .0. , .0. >. -> -. ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) ) )
40 39 imp 
 |-  ( ( p e. ( ran F X. ran G ) /\ -. p = <. .0. , .0. >. ) -> -. ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) )
41 28 36 40 syl2anc 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> -. ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) )
42 ianor 
 |-  ( -. ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) <-> ( -. ( 1st ` p ) = .0. \/ -. ( 2nd ` p ) = .0. ) )
43 df-ne 
 |-  ( ( 1st ` p ) =/= .0. <-> -. ( 1st ` p ) = .0. )
44 df-ne 
 |-  ( ( 2nd ` p ) =/= .0. <-> -. ( 2nd ` p ) = .0. )
45 43 44 orbi12i 
 |-  ( ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) <-> ( -. ( 1st ` p ) = .0. \/ -. ( 2nd ` p ) = .0. ) )
46 42 45 bitr4i 
 |-  ( -. ( ( 1st ` p ) = .0. /\ ( 2nd ` p ) = .0. ) <-> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) )
47 41 46 sylib 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) )
48 1 2 3 4 5 6 7 8 12 13 9 11 sibfinima 
 |-  ( ( ( ph /\ ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) /\ ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) )
49 17 30 32 47 48 syl31anc 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) )
50 fnfvima 
 |-  ( ( H Fn RR /\ ( 0 [,) +oo ) C_ RR /\ ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) ) -> ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) e. ( H " ( 0 [,) +oo ) ) )
51 24 26 49 50 syl3anc 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) e. ( H " ( 0 [,) +oo ) ) )
52 imassrn 
 |-  ( H " ( 0 [,) +oo ) ) C_ ran H
53 22 frnd 
 |-  ( ph -> ran H C_ ( Base ` ( Scalar ` W ) ) )
54 52 53 sstrid 
 |-  ( ph -> ( H " ( 0 [,) +oo ) ) C_ ( Base ` ( Scalar ` W ) ) )
55 eqid 
 |-  ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) = ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) )
56 55 18 ressbas2 
 |-  ( ( H " ( 0 [,) +oo ) ) C_ ( Base ` ( Scalar ` W ) ) -> ( H " ( 0 [,) +oo ) ) = ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) ) )
57 54 56 syl 
 |-  ( ph -> ( H " ( 0 [,) +oo ) ) = ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) ) )
58 17 57 syl 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( H " ( 0 [,) +oo ) ) = ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) ) )
59 51 58 eleqtrd 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) e. ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) ) )
60 1 2 3 4 5 6 7 8 13 sibff 
 |-  ( ph -> G : U. dom M --> U. J )
61 1 2 tpsuni 
 |-  ( W e. TopSp -> B = U. J )
62 feq3 
 |-  ( B = U. J -> ( G : U. dom M --> B <-> G : U. dom M --> U. J ) )
63 9 61 62 3syl 
 |-  ( ph -> ( G : U. dom M --> B <-> G : U. dom M --> U. J ) )
64 60 63 mpbird 
 |-  ( ph -> G : U. dom M --> B )
65 64 frnd 
 |-  ( ph -> ran G C_ B )
66 65 adantr 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ran G C_ B )
67 66 32 sseldd 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( 2nd ` p ) e. B )
68 6 fvexi 
 |-  H e. _V
69 imaexg 
 |-  ( H e. _V -> ( H " ( 0 [,) +oo ) ) e. _V )
70 eqid 
 |-  ( W |`v ( H " ( 0 [,) +oo ) ) ) = ( W |`v ( H " ( 0 [,) +oo ) ) )
71 70 1 resvbas 
 |-  ( ( H " ( 0 [,) +oo ) ) e. _V -> B = ( Base ` ( W |`v ( H " ( 0 [,) +oo ) ) ) ) )
72 68 69 71 mp2b 
 |-  B = ( Base ` ( W |`v ( H " ( 0 [,) +oo ) ) ) )
73 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
74 70 73 18 resvsca 
 |-  ( ( H " ( 0 [,) +oo ) ) e. _V -> ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) = ( Scalar ` ( W |`v ( H " ( 0 [,) +oo ) ) ) ) )
75 68 69 74 mp2b 
 |-  ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) = ( Scalar ` ( W |`v ( H " ( 0 [,) +oo ) ) ) )
76 70 5 resvvsca 
 |-  ( ( H " ( 0 [,) +oo ) ) e. _V -> .x. = ( .s ` ( W |`v ( H " ( 0 [,) +oo ) ) ) ) )
77 68 69 76 mp2b 
 |-  .x. = ( .s ` ( W |`v ( H " ( 0 [,) +oo ) ) ) )
78 eqid 
 |-  ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) ) = ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) )
79 72 75 77 78 slmdvscl 
 |-  ( ( ( W |`v ( H " ( 0 [,) +oo ) ) ) e. SLMod /\ ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) e. ( Base ` ( ( Scalar ` W ) |`s ( H " ( 0 [,) +oo ) ) ) ) /\ ( 2nd ` p ) e. B ) -> ( ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) .x. ( 2nd ` p ) ) e. B )
80 16 59 67 79 syl3anc 
 |-  ( ( ph /\ p e. ( ( ran F X. ran G ) \ { <. .0. , .0. >. } ) ) -> ( ( H ` ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) .x. ( 2nd ` p ) ) e. B )