Theorem xpssca

Description: Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	xpssca.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
	xpssca.g	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
	xpssca.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	xpssca.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
Assertion	xpssca	⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		xpssca.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2		xpssca.g	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
3		xpssca.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4		xpssca.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
5		eqid	⊢ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
6	2	fvexi	⊢ 𝐺 ∈ V
7	6	a1i	⊢ ( 𝜑 → 𝐺 ∈ V )
8		prex	⊢ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ∈ V
9	8	a1i	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ∈ V )
10	5 7 9	prdssca	⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
14	1 11 12 3 4 13 2 5	xpsval	⊢ ( 𝜑 → 𝑇 = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
15	1 11 12 3 4 13 2 5	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
16	13	xpsff1o2	⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
17		f1ocnv	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
18	16 17	mp1i	⊢ ( 𝜑 → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
19		f1ofo	⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
20	18 19	syl	⊢ ( 𝜑 → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
21		ovexd	⊢ ( 𝜑 → ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
22		eqid	⊢ ( Scalar ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Scalar ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
23	14 15 20 21 22	imassca	⊢ ( 𝜑 → ( Scalar ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Scalar ‘ 𝑇 ) )
24	10 23	eqtrd	⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝑇 ) )