rrxprds

Description: Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
	rrxbase.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	rrxprds	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) ↾_s 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2		rrxbase.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
3	1	rrxval	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
4		refld	⊢ ℝ_fld ∈ Field
5		eqid	⊢ ( ℝ_fld freeLMod 𝐼 ) = ( ℝ_fld freeLMod 𝐼 )
6		eqid	⊢ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) )
7	5 6	frlmpws	⊢ ( ( ℝ_fld ∈ Field ∧ 𝐼 ∈ 𝑉 ) → ( ℝ_fld freeLMod 𝐼 ) = ( ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) ↾_s ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
8	4 7	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ_fld freeLMod 𝐼 ) = ( ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) ↾_s ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
9		fvex	⊢ ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) ∈ V
10		rlmval	⊢ ( ringLMod ‘ ℝ_fld ) = ( ( subringAlg ‘ ℝ_fld ) ‘ ( Base ‘ ℝ_fld ) )
11		rebase	⊢ ℝ = ( Base ‘ ℝ_fld )
12	11	fveq2i	⊢ ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) = ( ( subringAlg ‘ ℝ_fld ) ‘ ( Base ‘ ℝ_fld ) )
13	10 12	eqtr4i	⊢ ( ringLMod ‘ ℝ_fld ) = ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ )
14	13	oveq1i	⊢ ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) = ( ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) ↑_s 𝐼 )
15	11	ressid	⊢ ( ℝ_fld ∈ Field → ( ℝ_fld ↾_s ℝ ) = ℝ_fld )
16	4 15	ax-mp	⊢ ( ℝ_fld ↾_s ℝ ) = ℝ_fld
17		eqidd	⊢ ( ⊤ → ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) = ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) )
18	11	eqimssi	⊢ ℝ ⊆ ( Base ‘ ℝ_fld )
19	18	a1i	⊢ ( ⊤ → ℝ ⊆ ( Base ‘ ℝ_fld ) )
20	17 19	srasca	⊢ ( ⊤ → ( ℝ_fld ↾_s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) ) )
21	20	mptru	⊢ ( ℝ_fld ↾_s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) )
22	16 21	eqtr3i	⊢ ℝ_fld = ( Scalar ‘ ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) )
23	14 22	pwsval	⊢ ( ( ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) = ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) )
24	9 23	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) = ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) )
25	24	eqcomd	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) = ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) )
26	3	fveq2d	⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
27		eqid	⊢ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) )
28	27 6	tcphbas	⊢ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
29	26 2 28	3eqtr4g	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
30	25 29	oveq12d	⊢ ( 𝐼 ∈ 𝑉 → ( ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) ↾_s 𝐵 ) = ( ( ( ringLMod ‘ ℝ_fld ) ↑_s 𝐼 ) ↾_s ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ) )
31	8 30	eqtr4d	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ_fld freeLMod 𝐼 ) = ( ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) ↾_s 𝐵 ) )
32	31	fveq2d	⊢ ( 𝐼 ∈ 𝑉 → ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) ↾_s 𝐵 ) ) )
33	3 32	eqtrd	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ( ℝ_fld X_s ( 𝐼 × { ( ( subringAlg ‘ ℝ_fld ) ‘ ℝ ) } ) ) ↾_s 𝐵 ) ) )

Metamath Proof Explorer

Theorem rrxprds

Proof