Theorem qusval 17433

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

Hypotheses

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

Assertion

Ref	Expression
qusval	⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))

Distinct variable groups:   𝑥, ∼   𝜑,𝑥   𝑥,𝑅   𝑥,𝑉

Allowed substitution hints:   𝑈(𝑥)   𝐹(𝑥)   𝑊(𝑥)   𝑍(𝑥)

Proof of Theorem qusval

Dummy variables 𝑒 𝑟 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3433   ↦ cmpt 5169  ‘cfv 6476  (class class class)co 7340   ∈ cmpo 7342  [cec 8614  Basecbs 17107   “_s cimas 17395   /_s cqus 17396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pr 5367

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-iota 6432  df-fun 6478  df-fv 6484  df-ov 7343  df-oprab 7344  df-mpo 7345  df-ec 8618  df-qus 17400

This theorem is referenced by:  qusin  17435  qusbas  17436  quss  17437  qusaddval  17444  qusaddf  17445  qusmulval  17446  qusmulf  17447  qusgrp2  18924  qusrng  20052  qusring2  20206  qustps  23591  qustgpopn  23989  qustgplem  23990  qustgphaus  23992  qusvsval  33285  quslmod  33291  quslmhm  33292