Theorem imasvscaf

Description: The image structure's scalar multiplication is closed in the base set. (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	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑝 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
	imasvscaf.c	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
Assertion	imasvscaf	⊢ ( 𝜑 → ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )

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		imasvscaf.c	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 )
11	1 2 3 4 5 6 7 8 9	imasvscafn	⊢ ( 𝜑 → ∙ Fn ( 𝐾 × 𝐵 ) )
12	1 2 3 4 5 6 7 8	imasvsca	⊢ ( 𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
13		fof	⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
14	3 13	syl	⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
15	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ ( 𝑝 · 𝑞 ) ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
16	10 15	syldan	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
17	16	ralrimivw	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉 ) ) → ∀ 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
18	17	anass1rs	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) ∧ 𝑝 ∈ 𝐾 ) → ∀ 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
19	18	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ∀ 𝑝 ∈ 𝐾 ∀ 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 )
20		eqid	⊢ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) = ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) )
21	20	fmpo	⊢ ( ∀ 𝑝 ∈ 𝐾 ∀ 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ 𝐵 ↔ ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⟶ 𝐵 )
22	19 21	sylib	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⟶ 𝐵 )
23		fssxp	⊢ ( ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) : ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⟶ 𝐵 → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × 𝐵 ) )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × 𝐵 ) )
25	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 )
26	25	snssd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → { ( 𝐹 ‘ 𝑞 ) } ⊆ 𝐵 )
27		xpss2	⊢ ( { ( 𝐹 ‘ 𝑞 ) } ⊆ 𝐵 → ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⊆ ( 𝐾 × 𝐵 ) )
28		xpss1	⊢ ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) ⊆ ( 𝐾 × 𝐵 ) → ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × 𝐵 ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
29	26 27 28	3syl	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( ( 𝐾 × { ( 𝐹 ‘ 𝑞 ) } ) × 𝐵 ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
30	24 29	sstrd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
31	30	ralrimiva	⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
32		iunss	⊢ ( ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) ↔ ∀ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
33	31 32	sylibr	⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ 𝐾 , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
34	12 33	eqsstrd	⊢ ( 𝜑 → ∙ ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) )
35		dff2	⊢ ( ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 ↔ ( ∙ Fn ( 𝐾 × 𝐵 ) ∧ ∙ ⊆ ( ( 𝐾 × 𝐵 ) × 𝐵 ) ) )
36	11 34 35	sylanbrc	⊢ ( 𝜑 → ∙ : ( 𝐾 × 𝐵 ) ⟶ 𝐵 )