Theorem sitgaddlemb

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

	Ref	Expression
Hypotheses	sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
	sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
	sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
	sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	sitgadd.1	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
	sitgadd.2	⊢ ( 𝜑 → ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ∈ SLMod )
	sitgadd.3	⊢ ( 𝜑 → 𝐽 ∈ Fre )
	sitgadd.4	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sitgadd.5	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sitgadd.6	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ ℝExt )
	sitgadd.7	⊢ + = ( +g ‘ 𝑊 )
Assertion	sitgaddlemb	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) · ( 2nd ‘ 𝑝 ) ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9		sitgadd.1	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
10		sitgadd.2	⊢ ( 𝜑 → ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ∈ SLMod )
11		sitgadd.3	⊢ ( 𝜑 → 𝐽 ∈ Fre )
12		sitgadd.4	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
13		sitgadd.5	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
14		sitgadd.6	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ ℝExt )
15		sitgadd.7	⊢ + = ( +g ‘ 𝑊 )
16	10	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ∈ SLMod )
17		simpl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → 𝜑 )
18		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
19	18	rrhfe	⊢ ( ( Scalar ‘ 𝑊 ) ∈ ℝExt → ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20	14 19	syl	⊢ ( 𝜑 → ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21	6	feq1i	⊢ ( 𝐻 : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( ℝHom ‘ ( Scalar ‘ 𝑊 ) ) : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
22	20 21	sylibr	⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23	22	ffnd	⊢ ( 𝜑 → 𝐻 Fn ℝ )
24	17 23	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → 𝐻 Fn ℝ )
25		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
26	25	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 0 [,) +∞ ) ⊆ ℝ )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) )
28	27	eldifad	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) )
29		xp1st	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) → ( 1st ‘ 𝑝 ) ∈ ran 𝐹 )
30	28 29	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 1st ‘ 𝑝 ) ∈ ran 𝐹 )
31		xp2nd	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) → ( 2nd ‘ 𝑝 ) ∈ ran 𝐺 )
32	28 31	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 2nd ‘ 𝑝 ) ∈ ran 𝐺 )
33	27	eldifbd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ¬ 𝑝 ∈ { ⟨ 0 , 0 ⟩ } )
34		velsn	⊢ ( 𝑝 ∈ { ⟨ 0 , 0 ⟩ } ↔ 𝑝 = ⟨ 0 , 0 ⟩ )
35	34	notbii	⊢ ( ¬ 𝑝 ∈ { ⟨ 0 , 0 ⟩ } ↔ ¬ 𝑝 = ⟨ 0 , 0 ⟩ )
36	33 35	sylib	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ¬ 𝑝 = ⟨ 0 , 0 ⟩ )
37		eqopi	⊢ ( ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ∧ ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) ) → 𝑝 = ⟨ 0 , 0 ⟩ )
38	37	ex	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) → ( ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) → 𝑝 = ⟨ 0 , 0 ⟩ ) )
39	38	con3d	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) → ( ¬ 𝑝 = ⟨ 0 , 0 ⟩ → ¬ ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) ) )
40	39	imp	⊢ ( ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ∧ ¬ 𝑝 = ⟨ 0 , 0 ⟩ ) → ¬ ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) )
41	28 36 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ¬ ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) )
42		ianor	⊢ ( ¬ ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) ↔ ( ¬ ( 1st ‘ 𝑝 ) = 0 ∨ ¬ ( 2nd ‘ 𝑝 ) = 0 ) )
43		df-ne	⊢ ( ( 1st ‘ 𝑝 ) ≠ 0 ↔ ¬ ( 1st ‘ 𝑝 ) = 0 )
44		df-ne	⊢ ( ( 2nd ‘ 𝑝 ) ≠ 0 ↔ ¬ ( 2nd ‘ 𝑝 ) = 0 )
45	43 44	orbi12i	⊢ ( ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ↔ ( ¬ ( 1st ‘ 𝑝 ) = 0 ∨ ¬ ( 2nd ‘ 𝑝 ) = 0 ) )
46	42 45	bitr4i	⊢ ( ¬ ( ( 1st ‘ 𝑝 ) = 0 ∧ ( 2nd ‘ 𝑝 ) = 0 ) ↔ ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) )
47	41 46	sylib	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) )
48	1 2 3 4 5 6 7 8 12 13 9 11	sibfinima	⊢ ( ( ( 𝜑 ∧ ( 1st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2nd ‘ 𝑝 ) ∈ ran 𝐺 ) ∧ ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ) → ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ( 0 [,) +∞ ) )
49	17 30 32 47 48	syl31anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ( 0 [,) +∞ ) )
50		fnfvima	⊢ ( ( 𝐻 Fn ℝ ∧ ( 0 [,) +∞ ) ⊆ ℝ ∧ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ( 0 [,) +∞ ) ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) )
51	24 26 49 50	syl3anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) ∈ ( 𝐻 “ ( 0 [,) +∞ ) ) )
52		imassrn	⊢ ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ran 𝐻
53	22	frnd	⊢ ( 𝜑 → ran 𝐻 ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
54	52 53	sstrid	⊢ ( 𝜑 → ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
55		eqid	⊢ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) = ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) )
56	55 18	ressbas2	⊢ ( ( 𝐻 “ ( 0 [,) +∞ ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝐻 “ ( 0 [,) +∞ ) ) = ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
57	54 56	syl	⊢ ( 𝜑 → ( 𝐻 “ ( 0 [,) +∞ ) ) = ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
58	17 57	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 𝐻 “ ( 0 [,) +∞ ) ) = ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
59	51 58	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) ∈ ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
60	1 2 3 4 5 6 7 8 13	sibff	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )
61	1 2	tpsuni	⊢ ( 𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽 )
62		feq3	⊢ ( 𝐵 = ∪ 𝐽 → ( 𝐺 : ∪ dom 𝑀 ⟶ 𝐵 ↔ 𝐺 : ∪ dom 𝑀 ⟶ ∪ 𝐽 ) )
63	9 61 62	3syl	⊢ ( 𝜑 → ( 𝐺 : ∪ dom 𝑀 ⟶ 𝐵 ↔ 𝐺 : ∪ dom 𝑀 ⟶ ∪ 𝐽 ) )
64	60 63	mpbird	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ 𝐵 )
65	64	frnd	⊢ ( 𝜑 → ran 𝐺 ⊆ 𝐵 )
66	65	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ran 𝐺 ⊆ 𝐵 )
67	66 32	sseldd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( 2nd ‘ 𝑝 ) ∈ 𝐵 )
68	6	fvexi	⊢ 𝐻 ∈ V
69		imaexg	⊢ ( 𝐻 ∈ V → ( 𝐻 “ ( 0 [,) +∞ ) ) ∈ V )
70		eqid	⊢ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) = ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) )
71	70 1	resvbas	⊢ ( ( 𝐻 “ ( 0 [,) +∞ ) ) ∈ V → 𝐵 = ( Base ‘ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
72	68 69 71	mp2b	⊢ 𝐵 = ( Base ‘ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
73		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
74	70 73 18	resvsca	⊢ ( ( 𝐻 “ ( 0 [,) +∞ ) ) ∈ V → ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) = ( Scalar ‘ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
75	68 69 74	mp2b	⊢ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) = ( Scalar ‘ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
76	70 5	resvvsca	⊢ ( ( 𝐻 “ ( 0 [,) +∞ ) ) ∈ V → · = ( ·𝑠 ‘ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) )
77	68 69 76	mp2b	⊢ · = ( ·𝑠 ‘ ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
78		eqid	⊢ ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) )
79	72 75 77 78	slmdvscl	⊢ ( ( ( 𝑊 ↾v ( 𝐻 “ ( 0 [,) +∞ ) ) ) ∈ SLMod ∧ ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) ∈ ( Base ‘ ( ( Scalar ‘ 𝑊 ) ↾s ( 𝐻 “ ( 0 [,) +∞ ) ) ) ) ∧ ( 2nd ‘ 𝑝 ) ∈ 𝐵 ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) · ( 2nd ‘ 𝑝 ) ) ∈ 𝐵 )
80	16 59 67 79	syl3anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ran 𝐹 × ran 𝐺 ) ∖ { ⟨ 0 , 0 ⟩ } ) ) → ( ( 𝐻 ‘ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ) · ( 2nd ‘ 𝑝 ) ) ∈ 𝐵 )