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 ⊢ φ → U = R / 𝑠 ∼ ˙
qusval.v ⊢ φ → V = Base R
qusval.f ⊢ F = x ∈ V ⟼ x ∼ ˙
qusval.e ⊢ φ → ∼ ˙ ∈ W
qusval.r ⊢ φ → R ∈ Z
Assertion qusval ⊢ φ → U = F “ 𝑠 R

Proof

Step Hyp Ref Expression
1 qusval.u ⊢ φ → U = R / 𝑠 ∼ ˙
2 qusval.v ⊢ φ → V = Base R
3 qusval.f ⊢ F = x ∈ V ⟼ x ∼ ˙
4 qusval.e ⊢ φ → ∼ ˙ ∈ W
5 qusval.r ⊢ φ → R ∈ Z
6 df-qus ⊢ / 𝑠 = r ∈ V , e ∈ V ⟼ x ∈ Base r ⟼ x e “ 𝑠 r
7 6 a1i ⊢ φ → / 𝑠 = r ∈ V , e ∈ V ⟼ x ∈ Base r ⟼ x e “ 𝑠 r
8 simprl ⊢ φ ∧ r = R ∧ e = ∼ ˙ → r = R
9 8 fveq2d ⊢ φ ∧ r = R ∧ e = ∼ ˙ → Base r = Base R
10 2 adantr ⊢ φ ∧ r = R ∧ e = ∼ ˙ → V = Base R
11 9 10 eqtr4d ⊢ φ ∧ r = R ∧ e = ∼ ˙ → Base r = V
12 eceq2 ⊢ e = ∼ ˙ → x e = x ∼ ˙
13 12 ad2antll ⊢ φ ∧ r = R ∧ e = ∼ ˙ → x e = x ∼ ˙
14 11 13 mpteq12dv ⊢ φ ∧ r = R ∧ e = ∼ ˙ → x ∈ Base r ⟼ x e = x ∈ V ⟼ x ∼ ˙
15 14 3 eqtr4di ⊢ φ ∧ r = R ∧ e = ∼ ˙ → x ∈ Base r ⟼ x e = F
16 15 8 oveq12d ⊢ φ ∧ r = R ∧ e = ∼ ˙ → x ∈ Base r ⟼ x e “ 𝑠 r = F “ 𝑠 R
17 5 elexd ⊢ φ → R ∈ V
18 4 elexd ⊢ φ → ∼ ˙ ∈ V
19 ovexd ⊢ φ → F “ 𝑠 R ∈ V
20 7 16 17 18 19 ovmpod ⊢ φ → R / 𝑠 ∼ ˙ = F “ 𝑠 R
21 1 20 eqtrd ⊢ φ → U = F “ 𝑠 R