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

Metamath Proof Explorer

Theorem uvcvvcl2

Description: A unit vector coordinate is a ring element. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses uvcvvcl2.u ⊢ U = R unitVec I
uvcvvcl2.b ⊢ B = Base R
uvcvvcl2.r ⊢ φ → R ∈ Ring
uvcvvcl2.i ⊢ φ → I ∈ W
uvcvvcl2.j ⊢ φ → J ∈ I
uvcvvcl2.k ⊢ φ → K ∈ I
Assertion uvcvvcl2 ⊢ φ → U ⁡ J ⁡ K ∈ B

Proof

Step Hyp Ref Expression
1 uvcvvcl2.u ⊢ U = R unitVec I
2 uvcvvcl2.b ⊢ B = Base R
3 uvcvvcl2.r ⊢ φ → R ∈ Ring
4 uvcvvcl2.i ⊢ φ → I ∈ W
5 uvcvvcl2.j ⊢ φ → J ∈ I
6 uvcvvcl2.k ⊢ φ → K ∈ I
7 eqid ⊢ 1 R = 1 R
8 eqid ⊢ 0 R = 0 R
9 1 7 8 uvcvval ⊢ R ∈ Ring ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → U ⁡ J ⁡ K = if K = J 1 R 0 R
10 3 4 5 6 9 syl31anc ⊢ φ → U ⁡ J ⁡ K = if K = J 1 R 0 R
11 2 7 ringidcl ⊢ R ∈ Ring → 1 R ∈ B
12 2 8 ring0cl ⊢ R ∈ Ring → 0 R ∈ B
13 11 12 ifcld ⊢ R ∈ Ring → if K = J 1 R 0 R ∈ B
14 3 13 syl ⊢ φ → if K = J 1 R 0 R ∈ B
15 10 14 eqeltrd ⊢ φ → U ⁡ J ⁡ K ∈ B