Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  linc1 Structured version   Visualization version   GIF version

Theorem linc1 47195
Description: A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.)
Hypotheses
Ref Expression
linc1.b 𝐡 = (Baseβ€˜π‘€)
linc1.s 𝑆 = (Scalarβ€˜π‘€)
linc1.0 0 = (0gβ€˜π‘†)
linc1.1 1 = (1rβ€˜π‘†)
linc1.f 𝐹 = (π‘₯ ∈ 𝑉 ↦ if(π‘₯ = 𝑋, 1 , 0 ))
Assertion
Ref Expression
linc1 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝐹( linC β€˜π‘€)𝑉) = 𝑋)
Distinct variable groups:   π‘₯,𝐡   π‘₯,𝑀   π‘₯,𝑉   π‘₯,𝑋   π‘₯, 0   π‘₯, 1
Allowed substitution hints:   𝑆(π‘₯)   𝐹(π‘₯)

Proof of Theorem linc1
Dummy variables 𝑣 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1134 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑀 ∈ LMod)
2 linc1.s . . . . . . . . . 10 𝑆 = (Scalarβ€˜π‘€)
32lmodring 20624 . . . . . . . . 9 (𝑀 ∈ LMod β†’ 𝑆 ∈ Ring)
42eqcomi 2739 . . . . . . . . . . . 12 (Scalarβ€˜π‘€) = 𝑆
54fveq2i 6895 . . . . . . . . . . 11 (Baseβ€˜(Scalarβ€˜π‘€)) = (Baseβ€˜π‘†)
6 linc1.1 . . . . . . . . . . 11 1 = (1rβ€˜π‘†)
75, 6ringidcl 20156 . . . . . . . . . 10 (𝑆 ∈ Ring β†’ 1 ∈ (Baseβ€˜(Scalarβ€˜π‘€)))
8 linc1.0 . . . . . . . . . . 11 0 = (0gβ€˜π‘†)
95, 8ring0cl 20157 . . . . . . . . . 10 (𝑆 ∈ Ring β†’ 0 ∈ (Baseβ€˜(Scalarβ€˜π‘€)))
107, 9jca 510 . . . . . . . . 9 (𝑆 ∈ Ring β†’ ( 1 ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ∧ 0 ∈ (Baseβ€˜(Scalarβ€˜π‘€))))
113, 10syl 17 . . . . . . . 8 (𝑀 ∈ LMod β†’ ( 1 ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ∧ 0 ∈ (Baseβ€˜(Scalarβ€˜π‘€))))
12113ad2ant1 1131 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ( 1 ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ∧ 0 ∈ (Baseβ€˜(Scalarβ€˜π‘€))))
1312adantr 479 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘₯ ∈ 𝑉) β†’ ( 1 ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ∧ 0 ∈ (Baseβ€˜(Scalarβ€˜π‘€))))
14 ifcl 4574 . . . . . 6 (( 1 ∈ (Baseβ€˜(Scalarβ€˜π‘€)) ∧ 0 ∈ (Baseβ€˜(Scalarβ€˜π‘€))) β†’ if(π‘₯ = 𝑋, 1 , 0 ) ∈ (Baseβ€˜(Scalarβ€˜π‘€)))
1513, 14syl 17 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘₯ ∈ 𝑉) β†’ if(π‘₯ = 𝑋, 1 , 0 ) ∈ (Baseβ€˜(Scalarβ€˜π‘€)))
16 linc1.f . . . . 5 𝐹 = (π‘₯ ∈ 𝑉 ↦ if(π‘₯ = 𝑋, 1 , 0 ))
1715, 16fmptd 7116 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝐹:π‘‰βŸΆ(Baseβ€˜(Scalarβ€˜π‘€)))
18 fvex 6905 . . . . 5 (Baseβ€˜(Scalarβ€˜π‘€)) ∈ V
19 simp2 1135 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑉 ∈ 𝒫 𝐡)
20 elmapg 8837 . . . . 5 (((Baseβ€˜(Scalarβ€˜π‘€)) ∈ V ∧ 𝑉 ∈ 𝒫 𝐡) β†’ (𝐹 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m 𝑉) ↔ 𝐹:π‘‰βŸΆ(Baseβ€˜(Scalarβ€˜π‘€))))
2118, 19, 20sylancr 585 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝐹 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m 𝑉) ↔ 𝐹:π‘‰βŸΆ(Baseβ€˜(Scalarβ€˜π‘€))))
2217, 21mpbird 256 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝐹 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m 𝑉))
23 linc1.b . . . . . . 7 𝐡 = (Baseβ€˜π‘€)
2423pweqi 4619 . . . . . 6 𝒫 𝐡 = 𝒫 (Baseβ€˜π‘€)
2524eleq2i 2823 . . . . 5 (𝑉 ∈ 𝒫 𝐡 ↔ 𝑉 ∈ 𝒫 (Baseβ€˜π‘€))
2625biimpi 215 . . . 4 (𝑉 ∈ 𝒫 𝐡 β†’ 𝑉 ∈ 𝒫 (Baseβ€˜π‘€))
27263ad2ant2 1132 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑉 ∈ 𝒫 (Baseβ€˜π‘€))
28 lincval 47179 . . 3 ((𝑀 ∈ LMod ∧ 𝐹 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Baseβ€˜π‘€)) β†’ (𝐹( linC β€˜π‘€)𝑉) = (𝑀 Ξ£g (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))))
291, 22, 27, 28syl3anc 1369 . 2 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝐹( linC β€˜π‘€)𝑉) = (𝑀 Ξ£g (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))))
30 eqid 2730 . . 3 (0gβ€˜π‘€) = (0gβ€˜π‘€)
31 lmodgrp 20623 . . . . 5 (𝑀 ∈ LMod β†’ 𝑀 ∈ Grp)
3231grpmndd 18870 . . . 4 (𝑀 ∈ LMod β†’ 𝑀 ∈ Mnd)
33323ad2ant1 1131 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑀 ∈ Mnd)
34 simp3 1136 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑋 ∈ 𝑉)
351adantr 479 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ 𝑀 ∈ LMod)
36 eqeq1 2734 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (π‘₯ = 𝑋 ↔ 𝑦 = 𝑋))
3736ifbid 4552 . . . . . . 7 (π‘₯ = 𝑦 β†’ if(π‘₯ = 𝑋, 1 , 0 ) = if(𝑦 = 𝑋, 1 , 0 ))
38 simpr 483 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ 𝑦 ∈ 𝑉)
39 eqid 2730 . . . . . . . . . . 11 (Baseβ€˜π‘†) = (Baseβ€˜π‘†)
402, 39, 6lmod1cl 20645 . . . . . . . . . 10 (𝑀 ∈ LMod β†’ 1 ∈ (Baseβ€˜π‘†))
41403ad2ant1 1131 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 1 ∈ (Baseβ€˜π‘†))
4241adantr 479 . . . . . . . 8 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ 1 ∈ (Baseβ€˜π‘†))
432, 39, 8lmod0cl 20644 . . . . . . . . . 10 (𝑀 ∈ LMod β†’ 0 ∈ (Baseβ€˜π‘†))
44433ad2ant1 1131 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 0 ∈ (Baseβ€˜π‘†))
4544adantr 479 . . . . . . . 8 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ 0 ∈ (Baseβ€˜π‘†))
4642, 45ifcld 4575 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ if(𝑦 = 𝑋, 1 , 0 ) ∈ (Baseβ€˜π‘†))
4716, 37, 38, 46fvmptd3 7022 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ (πΉβ€˜π‘¦) = if(𝑦 = 𝑋, 1 , 0 ))
4847, 46eqeltrd 2831 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ (πΉβ€˜π‘¦) ∈ (Baseβ€˜π‘†))
49 elelpwi 4613 . . . . . . . 8 ((𝑦 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐡) β†’ 𝑦 ∈ 𝐡)
5049expcom 412 . . . . . . 7 (𝑉 ∈ 𝒫 𝐡 β†’ (𝑦 ∈ 𝑉 β†’ 𝑦 ∈ 𝐡))
51503ad2ant2 1132 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝑦 ∈ 𝑉 β†’ 𝑦 ∈ 𝐡))
5251imp 405 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ 𝑦 ∈ 𝐡)
53 eqid 2730 . . . . . 6 ( ·𝑠 β€˜π‘€) = ( ·𝑠 β€˜π‘€)
5423, 2, 53, 39lmodvscl 20634 . . . . 5 ((𝑀 ∈ LMod ∧ (πΉβ€˜π‘¦) ∈ (Baseβ€˜π‘†) ∧ 𝑦 ∈ 𝐡) β†’ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦) ∈ 𝐡)
5535, 48, 52, 54syl3anc 1369 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑦 ∈ 𝑉) β†’ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦) ∈ 𝐡)
56 eqid 2730 . . . 4 (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦)) = (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))
5755, 56fmptd 7116 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦)):π‘‰βŸΆπ΅)
58 fveq2 6892 . . . . . . 7 (𝑦 = 𝑣 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘£))
59 id 22 . . . . . . 7 (𝑦 = 𝑣 β†’ 𝑦 = 𝑣)
6058, 59oveq12d 7431 . . . . . 6 (𝑦 = 𝑣 β†’ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦) = ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣))
6160cbvmptv 5262 . . . . 5 (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦)) = (𝑣 ∈ 𝑉 ↦ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣))
62 fvexd 6907 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (0gβ€˜π‘€) ∈ V)
63 ovexd 7448 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) β†’ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) ∈ V)
6461, 19, 62, 63mptsuppd 8176 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ((𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦)) supp (0gβ€˜π‘€)) = {𝑣 ∈ 𝑉 ∣ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€)})
65 2a1 28 . . . . . . 7 (𝑣 = 𝑋 β†’ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) β†’ (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋)))
66 simprr 769 . . . . . . . . . . . . . 14 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ 𝑣 ∈ 𝑉)
676fvexi 6906 . . . . . . . . . . . . . . 15 1 ∈ V
688fvexi 6906 . . . . . . . . . . . . . . 15 0 ∈ V
6967, 68ifex 4579 . . . . . . . . . . . . . 14 if(𝑣 = 𝑋, 1 , 0 ) ∈ V
70 eqeq1 2734 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑣 β†’ (π‘₯ = 𝑋 ↔ 𝑣 = 𝑋))
7170ifbid 4552 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑣 β†’ if(π‘₯ = 𝑋, 1 , 0 ) = if(𝑣 = 𝑋, 1 , 0 ))
7271, 16fvmptg 6997 . . . . . . . . . . . . . 14 ((𝑣 ∈ 𝑉 ∧ if(𝑣 = 𝑋, 1 , 0 ) ∈ V) β†’ (πΉβ€˜π‘£) = if(𝑣 = 𝑋, 1 , 0 ))
7366, 69, 72sylancl 584 . . . . . . . . . . . . 13 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ (πΉβ€˜π‘£) = if(𝑣 = 𝑋, 1 , 0 ))
74 iffalse 4538 . . . . . . . . . . . . . 14 (Β¬ 𝑣 = 𝑋 β†’ if(𝑣 = 𝑋, 1 , 0 ) = 0 )
7574adantr 479 . . . . . . . . . . . . 13 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ if(𝑣 = 𝑋, 1 , 0 ) = 0 )
7673, 75eqtrd 2770 . . . . . . . . . . . 12 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ (πΉβ€˜π‘£) = 0 )
7776oveq1d 7428 . . . . . . . . . . 11 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) = ( 0 ( ·𝑠 β€˜π‘€)𝑣))
781adantr 479 . . . . . . . . . . . . 13 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) β†’ 𝑀 ∈ LMod)
7978adantl 480 . . . . . . . . . . . 12 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ 𝑀 ∈ LMod)
80 elelpwi 4613 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐡) β†’ 𝑣 ∈ 𝐡)
8180expcom 412 . . . . . . . . . . . . . . 15 (𝑉 ∈ 𝒫 𝐡 β†’ (𝑣 ∈ 𝑉 β†’ 𝑣 ∈ 𝐡))
82813ad2ant2 1132 . . . . . . . . . . . . . 14 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝑣 ∈ 𝑉 β†’ 𝑣 ∈ 𝐡))
8382imp 405 . . . . . . . . . . . . 13 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) β†’ 𝑣 ∈ 𝐡)
8483adantl 480 . . . . . . . . . . . 12 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ 𝑣 ∈ 𝐡)
8523, 2, 53, 8, 30lmod0vs 20651 . . . . . . . . . . . 12 ((𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐡) β†’ ( 0 ( ·𝑠 β€˜π‘€)𝑣) = (0gβ€˜π‘€))
8679, 84, 85syl2anc 582 . . . . . . . . . . 11 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ ( 0 ( ·𝑠 β€˜π‘€)𝑣) = (0gβ€˜π‘€))
8777, 86eqtrd 2770 . . . . . . . . . 10 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) = (0gβ€˜π‘€))
8887neeq1d 2998 . . . . . . . . 9 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) ↔ (0gβ€˜π‘€) β‰  (0gβ€˜π‘€)))
89 eqneqall 2949 . . . . . . . . . 10 ((0gβ€˜π‘€) = (0gβ€˜π‘€) β†’ ((0gβ€˜π‘€) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋))
9030, 89ax-mp 5 . . . . . . . . 9 ((0gβ€˜π‘€) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋)
9188, 90syl6bi 252 . . . . . . . 8 ((Β¬ 𝑣 = 𝑋 ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉)) β†’ (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋))
9291ex 411 . . . . . . 7 (Β¬ 𝑣 = 𝑋 β†’ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) β†’ (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋)))
9365, 92pm2.61i 182 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ 𝑣 ∈ 𝑉) β†’ (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋))
9493ralrimiva 3144 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ βˆ€π‘£ ∈ 𝑉 (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋))
95 rabsssn 4671 . . . . 5 ({𝑣 ∈ 𝑉 ∣ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€)} βŠ† {𝑋} ↔ βˆ€π‘£ ∈ 𝑉 (((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€) β†’ 𝑣 = 𝑋))
9694, 95sylibr 233 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ {𝑣 ∈ 𝑉 ∣ ((πΉβ€˜π‘£)( ·𝑠 β€˜π‘€)𝑣) β‰  (0gβ€˜π‘€)} βŠ† {𝑋})
9764, 96eqsstrd 4021 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ((𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦)) supp (0gβ€˜π‘€)) βŠ† {𝑋})
9823, 30, 33, 19, 34, 57, 97gsumpt 19873 . 2 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝑀 Ξ£g (𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))) = ((𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))β€˜π‘‹))
99 ovex 7446 . . . 4 ((πΉβ€˜π‘‹)( ·𝑠 β€˜π‘€)𝑋) ∈ V
100 fveq2 6892 . . . . . 6 (𝑦 = 𝑋 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘‹))
101 id 22 . . . . . 6 (𝑦 = 𝑋 β†’ 𝑦 = 𝑋)
102100, 101oveq12d 7431 . . . . 5 (𝑦 = 𝑋 β†’ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦) = ((πΉβ€˜π‘‹)( ·𝑠 β€˜π‘€)𝑋))
103102, 56fvmptg 6997 . . . 4 ((𝑋 ∈ 𝑉 ∧ ((πΉβ€˜π‘‹)( ·𝑠 β€˜π‘€)𝑋) ∈ V) β†’ ((𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))β€˜π‘‹) = ((πΉβ€˜π‘‹)( ·𝑠 β€˜π‘€)𝑋))
10434, 99, 103sylancl 584 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ((𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))β€˜π‘‹) = ((πΉβ€˜π‘‹)( ·𝑠 β€˜π‘€)𝑋))
105 iftrue 4535 . . . . . 6 (π‘₯ = 𝑋 β†’ if(π‘₯ = 𝑋, 1 , 0 ) = 1 )
106105, 16fvmptg 6997 . . . . 5 ((𝑋 ∈ 𝑉 ∧ 1 ∈ V) β†’ (πΉβ€˜π‘‹) = 1 )
10734, 67, 106sylancl 584 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (πΉβ€˜π‘‹) = 1 )
108107oveq1d 7428 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ((πΉβ€˜π‘‹)( ·𝑠 β€˜π‘€)𝑋) = ( 1 ( ·𝑠 β€˜π‘€)𝑋))
109 elelpwi 4613 . . . . . 6 ((𝑋 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐡) β†’ 𝑋 ∈ 𝐡)
110109ancoms 457 . . . . 5 ((𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑋 ∈ 𝐡)
1111103adant1 1128 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ 𝑋 ∈ 𝐡)
11223, 2, 53, 6lmodvs1 20646 . . . 4 ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐡) β†’ ( 1 ( ·𝑠 β€˜π‘€)𝑋) = 𝑋)
1131, 111, 112syl2anc 582 . . 3 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ( 1 ( ·𝑠 β€˜π‘€)𝑋) = 𝑋)
114104, 108, 1133eqtrd 2774 . 2 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ ((𝑦 ∈ 𝑉 ↦ ((πΉβ€˜π‘¦)( ·𝑠 β€˜π‘€)𝑦))β€˜π‘‹) = 𝑋)
11529, 98, 1143eqtrd 2774 1 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝐹( linC β€˜π‘€)𝑉) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  {crab 3430  Vcvv 3472   βŠ† wss 3949  ifcif 4529  π’« cpw 4603  {csn 4629   ↦ cmpt 5232  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7413   supp csupp 8150   ↑m cmap 8824  Basecbs 17150  Scalarcsca 17206   ·𝑠 cvsca 17207  0gc0g 17391   Ξ£g cgsu 17392  Mndcmnd 18661  1rcur 20077  Ringcrg 20129  LModclmod 20616   linC clinc 47174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8151  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-er 8707  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9366  df-oi 9509  df-card 9938  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-nn 12219  df-2 12281  df-n0 12479  df-z 12565  df-uz 12829  df-fz 13491  df-fzo 13634  df-seq 13973  df-hash 14297  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17151  df-ress 17180  df-plusg 17216  df-0g 17393  df-gsum 17394  df-mre 17536  df-mrc 17537  df-acs 17539  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-submnd 18708  df-grp 18860  df-mulg 18989  df-cntz 19224  df-cmn 19693  df-mgp 20031  df-ur 20078  df-ring 20131  df-lmod 20618  df-linc 47176
This theorem is referenced by:  lcoss  47206
  Copyright terms: Public domain W3C validator