Theorem imasvscaval

Description: The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasvscaf.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
	imasvscaf.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasvscaf.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imasvscaf.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
	imasvscaf.g	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
	imasvscaf.k	⊢ 𝐾 = ( Base ‘ 𝐺 )
	imasvscaf.q	⊢ · = ( ·𝑠 ‘ 𝑅 )
	imasvscaf.s	⊢ ∙ = ( ·𝑠 ‘ 𝑈 )
	imasvscaf.e	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
Assertion	imasvscaval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imasvscaf.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2		imasvscaf.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasvscaf.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imasvscaf.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		imasvscaf.g	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
6		imasvscaf.k	⊢ 𝐾 = ( Base ‘ 𝐺 )
7		imasvscaf.q	⊢ · = ( ·𝑠 ‘ 𝑅 )
8		imasvscaf.s	⊢ ∙ = ( ·𝑠 ‘ 𝑈 )
9		imasvscaf.e	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
10	1 2 3 4 5 6 7 8 9	imasvscafn	⊢ ( 𝜑 → ∙ Fn ( 𝐾 × 𝐵 ) )
11		fnfun	⊢ ( ∙ Fn ( 𝐾 × 𝐵 ) → Fun ∙ )
12	10 11	syl	⊢ ( 𝜑 → Fun ∙ )
13	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → Fun ∙ )
14		eqidd	⊢ ( 𝑞 = 𝑌 → 𝐾 = 𝐾 )
15		fveq2	⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑌 ) )
16	15	sneqd	⊢ ( 𝑞 = 𝑌 → { ( 𝐹 ‘ 𝑞 ) } = { ( 𝐹 ‘ 𝑌 ) } )
17		oveq2	⊢ ( 𝑞 = 𝑌 → ( 𝑝 · 𝑞 ) = ( 𝑝 · 𝑌 ) )
18	17	fveq2d	⊢ ( 𝑞 = 𝑌 → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) )
19	14 16 18	mpoeq123dv	⊢ ( 𝑞 = 𝑌 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) )
20	19	ssiun2s	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
21	20	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
22	1 2 3 4 5 6 7 8	imasvsca	⊢ ( 𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
23	22	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
24	21 23	sseqtrrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∙ )
25		simp2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐾 )
26		fvex	⊢ ( 𝐹 ‘ 𝑌 ) ∈ V
27	26	snid	⊢ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) }
28		opelxpi	⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) )
29	25 27 28	sylancl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } ) )
30		eqid	⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) )
31		fvex	⊢ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ∈ V
32	30 31	dmmpo	⊢ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) = ( 𝐾 × { ( 𝐹 ‘ 𝑌 ) } )
33	29 32	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) )
34		funssfv	⊢ ( ( Fun ∙ ∧ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ⊆ ∙ ∧ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ∈ dom ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ) → ( ∙ ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) )
35	13 24 33 34	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( ∙ ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ ) )
36		df-ov	⊢ ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( ∙ ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ )
37		df-ov	⊢ ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ‘ ⟨ 𝑋 , ( 𝐹 ‘ 𝑌 ) ⟩ )
38	35 36 37	3eqtr4g	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) )
39		fvoveq1	⊢ ( 𝑝 = 𝑋 → ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
40		eqidd	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑌 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
41		fvex	⊢ ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ∈ V
42	39 40 30 41	ovmpo	⊢ ( ( 𝑋 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑌 ) ∈ { ( 𝐹 ‘ 𝑌 ) } ) → ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
43	25 27 42	sylancl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑌 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑌 ) ) ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )
44	38 43	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )