Metamath Proof Explorer

Theorem uvcfval

Description: Value of the unit-vector generator for a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses uvcfval.u ⊢ U = R unitVec I
uvcfval.o ⊢ 1 ˙ = 1 R
uvcfval.z ⊢ 0 ˙ = 0 R
Assertion uvcfval ⊢ R ∈ V ∧ I ∈ W → U = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 uvcfval.u ⊢ U = R unitVec I
2 uvcfval.o ⊢ 1 ˙ = 1 R
3 uvcfval.z ⊢ 0 ˙ = 0 R
4 elex ⊢ R ∈ V → R ∈ V
5 elex ⊢ I ∈ W → I ∈ V
6 df-uvc ⊢ unitVec = r ∈ V , i ∈ V ⟼ j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r
7 6 a1i ⊢ R ∈ V ∧ I ∈ V → unitVec = r ∈ V , i ∈ V ⟼ j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r
8 simpr ⊢ r = R ∧ i = I → i = I
9 fveq2 ⊢ r = R → 1 r = 1 R
10 9 2 eqtr4di ⊢ r = R → 1 r = 1 ˙
11 fveq2 ⊢ r = R → 0 r = 0 R
12 11 3 eqtr4di ⊢ r = R → 0 r = 0 ˙
13 10 12 ifeq12d ⊢ r = R → if k = j 1 r 0 r = if k = j 1 ˙ 0 ˙
14 13 adantr ⊢ r = R ∧ i = I → if k = j 1 r 0 r = if k = j 1 ˙ 0 ˙
15 8 14 mpteq12dv ⊢ r = R ∧ i = I → k ∈ i ⟼ if k = j 1 r 0 r = k ∈ I ⟼ if k = j 1 ˙ 0 ˙
16 8 15 mpteq12dv ⊢ r = R ∧ i = I → j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙
17 16 adantl ⊢ R ∈ V ∧ I ∈ V ∧ r = R ∧ i = I → j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙
18 simpl ⊢ R ∈ V ∧ I ∈ V → R ∈ V
19 simpr ⊢ R ∈ V ∧ I ∈ V → I ∈ V
20 mptexg ⊢ I ∈ V → j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙ ∈ V
21 20 adantl ⊢ R ∈ V ∧ I ∈ V → j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙ ∈ V
22 7 17 18 19 21 ovmpod ⊢ R ∈ V ∧ I ∈ V → R unitVec I = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙
23 4 5 22 syl2an ⊢ R ∈ V ∧ I ∈ W → R unitVec I = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙
24 1 23 syl5eq ⊢ R ∈ V ∧ I ∈ W → U = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙