Theorem bj-isrvec

Description: The predicate "is a real vector space". Using df-sca instead of scaid shortens the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca . (Contributed by BJ, 6-Jan-2024)

	Ref	Expression
Assertion	bj-isrvec	⊢ ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-rvec	⊢ ℝ-Vec = ( LMod ∩ ( ◡ Scalar “ { ℝfld } ) )
2	1	elin2	⊢ ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ) )
3		scaid	⊢ Scalar = Slot ( Scalar ‘ ndx )
4	3	slotfn	⊢ Scalar Fn V
5		df-fn	⊢ ( Scalar Fn V ↔ ( Fun Scalar ∧ dom Scalar = V ) )
6	4 5	mpbi	⊢ ( Fun Scalar ∧ dom Scalar = V )
7		elex	⊢ ( 𝑉 ∈ LMod → 𝑉 ∈ V )
8		eleq2	⊢ ( dom Scalar = V → ( 𝑉 ∈ dom Scalar ↔ 𝑉 ∈ V ) )
9	7 8	syl5ibrcom	⊢ ( 𝑉 ∈ LMod → ( dom Scalar = V → 𝑉 ∈ dom Scalar ) )
10	9	anim2d	⊢ ( 𝑉 ∈ LMod → ( ( Fun Scalar ∧ dom Scalar = V ) → ( Fun Scalar ∧ 𝑉 ∈ dom Scalar ) ) )
11	6 10	mpi	⊢ ( 𝑉 ∈ LMod → ( Fun Scalar ∧ 𝑉 ∈ dom Scalar ) )
12		fvimacnv	⊢ ( ( Fun Scalar ∧ 𝑉 ∈ dom Scalar ) → ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ) )
13	11 12	syl	⊢ ( 𝑉 ∈ LMod → ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ) )
14		fvex	⊢ ( Scalar ‘ 𝑉 ) ∈ V
15	14	elsn	⊢ ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ ( Scalar ‘ 𝑉 ) = ℝfld )
16	13 15	bitr3di	⊢ ( 𝑉 ∈ LMod → ( 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ↔ ( Scalar ‘ 𝑉 ) = ℝfld ) )
17	16	pm5.32i	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ) ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )
18	2 17	bitri	⊢ ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )