Theorem bj-isrvec

Description: The predicate "is a real vector space". Using df-sca instead of scaid would shorten 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	|- ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-rvec	|- RRVec = ( LMod i^i ( `' Scalar " { RRfld } ) )
2	1	elin2	|- ( V e. RRVec <-> ( V e. LMod /\ V e. ( `' Scalar " { RRfld } ) ) )
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	|- ( V e. LMod -> V e. _V )
8		eleq2	|- ( dom Scalar = _V -> ( V e. dom Scalar <-> V e. _V ) )
9	7 8	syl5ibrcom	|- ( V e. LMod -> ( dom Scalar = _V -> V e. dom Scalar ) )
10	9	anim2d	|- ( V e. LMod -> ( ( Fun Scalar /\ dom Scalar = _V ) -> ( Fun Scalar /\ V e. dom Scalar ) ) )
11	6 10	mpi	|- ( V e. LMod -> ( Fun Scalar /\ V e. dom Scalar ) )
12		fvimacnv	|- ( ( Fun Scalar /\ V e. dom Scalar ) -> ( ( Scalar ` V ) e. { RRfld } <-> V e. ( `' Scalar " { RRfld } ) ) )
13	11 12	syl	|- ( V e. LMod -> ( ( Scalar ` V ) e. { RRfld } <-> V e. ( `' Scalar " { RRfld } ) ) )
14		fvex	|- ( Scalar ` V ) e. _V
15	14	elsn	|- ( ( Scalar ` V ) e. { RRfld } <-> ( Scalar ` V ) = RRfld )
16	13 15	bitr3di	|- ( V e. LMod -> ( V e. ( `' Scalar " { RRfld } ) <-> ( Scalar ` V ) = RRfld ) )
17	16	pm5.32i	|- ( ( V e. LMod /\ V e. ( `' Scalar " { RRfld } ) ) <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )
18	2 17	bitri	|- ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )