Metamath Proof Explorer

Theorem lcoop

Description: A linear combination as operation. (Contributed by AV, 5-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lcoop.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lcoop.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lcoop.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
Assertion lcoop ( ( 𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } )

Proof

Step Hyp Ref Expression
1 lcoop.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lcoop.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 lcoop.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
4 elex ⊢ ( 𝑀 ∈ 𝑋 → 𝑀 ∈ V )
5 4 adantr ⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑀 ∈ V )
6 1 pweqi ⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
7 6 eleq2i ⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
8 7 bilani ⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
9 1 fvexi ⊢ 𝐵 ∈ V
10 rabexg ⊢ ( 𝐵 ∈ V → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } ∈ V )
11 9 10 mp1i ⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵 ) → { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } ∈ V )
12 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
13 12 1 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
14 13 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( Base ‘ 𝑚 ) = 𝐵 )
15 2fveq3 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
16 15 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
17 2 fveq2i ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
18 3 17 eqtri ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
19 16 18 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = 𝑅 )
20 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → 𝑣 = 𝑉 )
21 19 20 oveq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) = ( 𝑅 ↑m 𝑉 ) )
22 2fveq3 ⊢ ( 𝑚 = 𝑀 → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
23 2 a1i ⊢ ( 𝑚 = 𝑀 → 𝑆 = ( Scalar ‘ 𝑀 ) )
24 23 eqcomd ⊢ ( 𝑚 = 𝑀 → ( Scalar ‘ 𝑀 ) = 𝑆 )
25 24 fveq2d ⊢ ( 𝑚 = 𝑀 → ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ 𝑆 ) )
26 22 25 eqtrd ⊢ ( 𝑚 = 𝑀 → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ 𝑆 ) )
27 26 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ 𝑆 ) )
28 27 breq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ↔ 𝑠 finSupp ( 0g ‘ 𝑆 ) ) )
29 fveq2 ⊢ ( 𝑚 = 𝑀 → ( linC ‘ 𝑚 ) = ( linC ‘ 𝑀 ) )
30 29 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( linC ‘ 𝑚 ) = ( linC ‘ 𝑀 ) )
31 eqidd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → 𝑠 = 𝑠 )
32 30 31 20 oveq123d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) )
33 32 eqeq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ↔ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
34 28 33 anbi12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) ↔ ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
35 21 34 rexeqbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → ( ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) ↔ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
36 14 35 rabeqbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = 𝑉 ) → { 𝑐 ∈ ( Base ‘ 𝑚 ) ∣ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) } = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } )
37 12 pweqd ⊢ ( 𝑚 = 𝑀 → 𝒫 ( Base ‘ 𝑚 ) = 𝒫 ( Base ‘ 𝑀 ) )
38 df-lco ⊢ LinCo = ( 𝑚 ∈ V , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑐 ∈ ( Base ‘ 𝑚 ) ∣ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑚 ) 𝑣 ) ) } )
39 36 37 38 ovmpox ⊢ ( ( 𝑀 ∈ V ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } ∈ V ) → ( 𝑀 LinCo 𝑉 ) = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } )
40 5 8 11 39 syl3anc ⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) = { 𝑐 ∈ 𝐵 ∣ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ 𝑆 ) ∧ 𝑐 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) } )