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 ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
uvcfval.o ⊢ 1 = ( 1r ‘ 𝑅 )
uvcfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion uvcfval ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 uvcfval.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2 uvcfval.o ⊢ 1 = ( 1r ‘ 𝑅 )
3 uvcfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
5 elex ⊢ ( 𝐼 ∈ 𝑊 → 𝐼 ∈ V )
6 df-uvc ⊢ unitVec = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
7 6 a1i ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → unitVec = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) ) )
8 simpr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
9 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
10 9 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 )
11 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
12 11 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
13 10 12 ifeq12d ⊢ ( 𝑟 = 𝑅 → if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) = if ( 𝑘 = 𝑗 , 1 , 0 ) )
14 13 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) = if ( 𝑘 = 𝑗 , 1 , 0 ) )
15 8 14 mpteq12dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) )
16 8 15 mpteq12dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )
17 16 adantl ⊢ ( ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) ∧ ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) ) → ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )
18 simpl ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → 𝑅 ∈ V )
19 simpr ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → 𝐼 ∈ V )
20 mptexg ⊢ ( 𝐼 ∈ V → ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) ∈ V )
21 20 adantl ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) ∈ V )
22 7 17 18 19 21 ovmpod ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → ( 𝑅 unitVec 𝐼 ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )
23 4 5 22 syl2an ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 unitVec 𝐼 ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )
24 1 23 syl5eq ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )