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