Description: The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | qusbas.u | ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) ) | |
qusbas.v | ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) | ||
qusbas.e | ⊢ ( 𝜑 → ∼ ∈ 𝑊 ) | ||
qusbas.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) | ||
quss.k | ⊢ 𝐾 = ( Scalar ‘ 𝑅 ) | ||
Assertion | quss | ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑈 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qusbas.u | ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) ) | |
2 | qusbas.v | ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) | |
3 | qusbas.e | ⊢ ( 𝜑 → ∼ ∈ 𝑊 ) | |
4 | qusbas.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) | |
5 | quss.k | ⊢ 𝐾 = ( Scalar ‘ 𝑅 ) | |
6 | eqid | ⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) | |
7 | 1 2 6 3 4 | qusval | ⊢ ( 𝜑 → 𝑈 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) “s 𝑅 ) ) |
8 | 1 2 6 3 4 | quslem | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) ) |
9 | 7 2 8 4 5 | imassca | ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑈 ) ) |