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 𝑅 ) )