Metamath Proof Explorer

Theorem uvcff

Description: Domain and codomain of the unit vector generator; ring condition required to be sure 1 and 0 are actually in the ring. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses uvcff.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
uvcff.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
uvcff.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion uvcff ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 uvcff.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2 uvcff.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
3 uvcff.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
4 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6 1 4 5 uvcfval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑈 = ( 𝑖 ∈ 𝐼 ↦ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 7 4 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
9 7 5 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
10 8 9 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
11 10 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
12 11 fmpttd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
13 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
14 elmapg ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
15 13 14 mpan ⊢ ( 𝐼 ∈ 𝑊 → ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
16 15 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
17 12 16 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
18 mptexg ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
19 18 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
20 funmpt ⊢ Fun ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
21 20 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → Fun ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
22 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
23 22 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( 0g ‘ 𝑅 ) ∈ V )
24 snfi ⊢ { 𝑖 } ∈ Fin
25 24 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → { 𝑖 } ∈ Fin )
26 eldifsni ⊢ ( 𝑗 ∈ ( 𝐼 ∖ { 𝑖 } ) → 𝑗 ≠ 𝑖 )
27 26 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝐼 ∖ { 𝑖 } ) ) → 𝑗 ≠ 𝑖 )
28 27 neneqd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝐼 ∖ { 𝑖 } ) ) → ¬ 𝑗 = 𝑖 )
29 28 iffalsed ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝐼 ∖ { 𝑖 } ) ) → if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
30 simplr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
31 29 30 suppss2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑖 } )
32 suppssfifsupp ⊢ ( ( ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) ∧ ( { 𝑖 } ∈ Fin ∧ ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑖 } ) ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
33 19 21 23 25 31 32 syl32anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
34 2 7 5 3 frlmelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐵 ↔ ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∧ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) ) ) )
35 34 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐵 ↔ ( ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∧ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) finSupp ( 0g ‘ 𝑅 ) ) ) )
36 17 33 35 mpbir2and ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐵 )
37 6 36 fmpt3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 ⟶ 𝐵 )