Theorem bj-isrvec

Description: The predicate "is a real vector space". (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		bj-evalfun	⊢ Fun Slot 5
4		df-sca	⊢ Scalar = Slot 5
5	4	funeqi	⊢ ( Fun Scalar ↔ Fun Slot 5 )
6	3 5	mpbir	⊢ Fun Scalar
7		0re	⊢ 0 ∈ ℝ
8	7	n0ii	⊢ ¬ ℝ = ∅
9		eqcom	⊢ ( ∅ = ℝ ↔ ℝ = ∅ )
10	8 9	mtbir	⊢ ¬ ∅ = ℝ
11		fveq2	⊢ ( ∅ = ℝfld → ( Base ‘ ∅ ) = ( Base ‘ ℝfld ) )
12		base0	⊢ ∅ = ( Base ‘ ∅ )
13		rebase	⊢ ℝ = ( Base ‘ ℝfld )
14	11 12 13	3eqtr4g	⊢ ( ∅ = ℝfld → ∅ = ℝ )
15	10 14	mto	⊢ ¬ ∅ = ℝfld
16		elsni	⊢ ( ∅ ∈ { ℝfld } → ∅ = ℝfld )
17	15 16	mto	⊢ ¬ ∅ ∈ { ℝfld }
18		bj-fvimacnv0	⊢ ( ( Fun Scalar ∧ ¬ ∅ ∈ { ℝfld } ) → ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ) )
19	6 17 18	mp2an	⊢ ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) )
20		fvex	⊢ ( Scalar ‘ 𝑉 ) ∈ V
21	20	elsn	⊢ ( ( Scalar ‘ 𝑉 ) ∈ { ℝfld } ↔ ( Scalar ‘ 𝑉 ) = ℝfld )
22	19 21	bitr3i	⊢ ( 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ↔ ( Scalar ‘ 𝑉 ) = ℝfld )
23	22	anbi2i	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑉 ∈ ( ◡ Scalar “ { ℝfld } ) ) ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )
24	2 23	bitri	⊢ ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )