Theorem lmodfopnelem2

Description: Lemma 2 for lmodfopne . (Contributed by AV, 2-Oct-2021)

	Ref	Expression
Hypotheses	lmodfopne.t	|- .x. = ( .sf ` W )
	lmodfopne.a	|- .+ = ( +f ` W )
	lmodfopne.v	|- V = ( Base ` W )
	lmodfopne.s	|- S = ( Scalar ` W )
	lmodfopne.k	|- K = ( Base ` S )
	lmodfopne.0	|- .0. = ( 0g ` S )
	lmodfopne.1	|- .1. = ( 1r ` S )
Assertion	lmodfopnelem2	|- ( ( W e. LMod /\ .+ = .x. ) -> ( .0. e. V /\ .1. e. V ) )

Proof

Step	Hyp	Ref	Expression
1		lmodfopne.t	|- .x. = ( .sf ` W )
2		lmodfopne.a	|- .+ = ( +f ` W )
3		lmodfopne.v	|- V = ( Base ` W )
4		lmodfopne.s	|- S = ( Scalar ` W )
5		lmodfopne.k	|- K = ( Base ` S )
6		lmodfopne.0	|- .0. = ( 0g ` S )
7		lmodfopne.1	|- .1. = ( 1r ` S )
8	1 2 3 4 5	lmodfopnelem1	|- ( ( W e. LMod /\ .+ = .x. ) -> V = K )
9	8	ex	|- ( W e. LMod -> ( .+ = .x. -> V = K ) )
10	4 5 6	lmod0cl	|- ( W e. LMod -> .0. e. K )
11	4 5 7	lmod1cl	|- ( W e. LMod -> .1. e. K )
12	10 11	jca	|- ( W e. LMod -> ( .0. e. K /\ .1. e. K ) )
13		eleq2	|- ( V = K -> ( .0. e. V <-> .0. e. K ) )
14		eleq2	|- ( V = K -> ( .1. e. V <-> .1. e. K ) )
15	13 14	anbi12d	|- ( V = K -> ( ( .0. e. V /\ .1. e. V ) <-> ( .0. e. K /\ .1. e. K ) ) )
16	12 15	syl5ibrcom	|- ( W e. LMod -> ( V = K -> ( .0. e. V /\ .1. e. V ) ) )
17	9 16	syld	|- ( W e. LMod -> ( .+ = .x. -> ( .0. e. V /\ .1. e. V ) ) )
18	17	imp	|- ( ( W e. LMod /\ .+ = .x. ) -> ( .0. e. V /\ .1. e. V ) )