Theorem sxbrsigalem6

Description: First direction for sxbrsiga , same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017)

	Ref	Expression
Hypothesis	sxbrsiga.0	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	sxbrsigalem6	$$⊢𝛔\left(J{\times }_{t}J\right)\subseteq {𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}$$

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		oveq1	$$⊢a=x\to \frac{a}{2^m}=\frac{x}{2^m}$$
3		oveq1	$$⊢a=x\to a+1=x+1$$
4	3	oveq1d	$$⊢a=x\to \frac{a+1}{2^m}=\frac{x+1}{2^m}$$
5	2 4	oveq12d	$$⊢a=x\to \left[\frac{a}{2^m},\frac{a+1}{2^m}\right)=\left[\frac{x}{2^m},\frac{x+1}{2^m}\right)$$
6		oveq2	$$⊢m=n\to 2^m=2^n$$
7	6	oveq2d	$$⊢m=n\to \frac{x}{2^m}=\frac{x}{2^n}$$
8	6	oveq2d	$$⊢m=n\to \frac{x+1}{2^m}=\frac{x+1}{2^n}$$
9	7 8	oveq12d	$$⊢m=n\to \left[\frac{x}{2^m},\frac{x+1}{2^m}\right)=\left[\frac{x}{2^n},\frac{x+1}{2^n}\right)$$
10	5 9	cbvmpov	$$⊢\left(a\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{a}{2^m},\frac{a+1}{2^m}\right)\right)=\left(x\in \mathbb{Z},n\in \mathbb{Z}⟼\left[\frac{x}{2^n},\frac{x+1}{2^n}\right)\right)$$
11		eqid	$$⊢\left(u\in \mathrm{ran}\left(a\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{a}{2^m},\frac{a+1}{2^m}\right)\right),v\in \mathrm{ran}\left(a\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{a}{2^m},\frac{a+1}{2^m}\right)\right)⟼u\times v\right)=\left(u\in \mathrm{ran}\left(a\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{a}{2^m},\frac{a+1}{2^m}\right)\right),v\in \mathrm{ran}\left(a\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{a}{2^m},\frac{a+1}{2^m}\right)\right)⟼u\times v\right)$$
12	1 10 11	sxbrsigalem5	$$⊢𝛔\left(J{\times }_{t}J\right)\subseteq {𝔅}_{ℝ}{\times }_s{𝔅}_{ℝ}$$