This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusval

Description: Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses qusval.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
qusval.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
qusval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
qusval.e ⊢ ( 𝜑 → ∼ ∈ 𝑊 )
qusval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
Assertion qusval ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )

Proof

Step Hyp Ref Expression
1 qusval.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2 qusval.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 qusval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
4 qusval.e ⊢ ( 𝜑 → ∼ ∈ 𝑊 )
5 qusval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
6 df-qus ⊢ /s = ( 𝑟 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 ) )
7 6 a1i ⊢ ( 𝜑 → /s = ( 𝑟 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 ) ) )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → 𝑟 = 𝑅 )
9 8 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
11 9 10 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → ( Base ‘ 𝑟 ) = 𝑉 )
12 eceq2 ⊢ ( 𝑒 = ∼ → [ 𝑥 ] 𝑒 = [ 𝑥 ] ∼ )
13 12 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → [ 𝑥 ] 𝑒 = [ 𝑥 ] ∼ )
14 11 13 mpteq12dv ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) )
15 14 3 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) = 𝐹 )
16 15 8 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑒 = ∼ ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 ) = ( 𝐹 “s 𝑅 ) )
17 5 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
18 4 elexd ⊢ ( 𝜑 → ∼ ∈ V )
19 ovexd ⊢ ( 𝜑 → ( 𝐹 “s 𝑅 ) ∈ V )
20 7 16 17 18 19 ovmpod ⊢ ( 𝜑 → ( 𝑅 /s ∼ ) = ( 𝐹 “s 𝑅 ) )
21 1 20 eqtrd ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )