Theorem lmodfopnelem2

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

	Ref	Expression
Hypotheses	lmodfopne.t	⊢ · = ( ·sf ‘ 𝑊 )
	lmodfopne.a	⊢ + = ( +𝑓 ‘ 𝑊 )
	lmodfopne.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmodfopne.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	lmodfopne.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	lmodfopne.0	⊢ 0 = ( 0g ‘ 𝑆 )
	lmodfopne.1	⊢ 1 = ( 1r ‘ 𝑆 )
Assertion	lmodfopnelem2	⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lmodfopne.t	⊢ · = ( ·sf ‘ 𝑊 )
2		lmodfopne.a	⊢ + = ( +𝑓 ‘ 𝑊 )
3		lmodfopne.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lmodfopne.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
5		lmodfopne.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		lmodfopne.0	⊢ 0 = ( 0g ‘ 𝑆 )
7		lmodfopne.1	⊢ 1 = ( 1r ‘ 𝑆 )
8	1 2 3 4 5	lmodfopnelem1	⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾 )
9	8	ex	⊢ ( 𝑊 ∈ LMod → ( + = · → 𝑉 = 𝐾 ) )
10	4 5 6	lmod0cl	⊢ ( 𝑊 ∈ LMod → 0 ∈ 𝐾 )
11	4 5 7	lmod1cl	⊢ ( 𝑊 ∈ LMod → 1 ∈ 𝐾 )
12	10 11	jca	⊢ ( 𝑊 ∈ LMod → ( 0 ∈ 𝐾 ∧ 1 ∈ 𝐾 ) )
13		eleq2	⊢ ( 𝑉 = 𝐾 → ( 0 ∈ 𝑉 ↔ 0 ∈ 𝐾 ) )
14		eleq2	⊢ ( 𝑉 = 𝐾 → ( 1 ∈ 𝑉 ↔ 1 ∈ 𝐾 ) )
15	13 14	anbi12d	⊢ ( 𝑉 = 𝐾 → ( ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ↔ ( 0 ∈ 𝐾 ∧ 1 ∈ 𝐾 ) ) )
16	12 15	syl5ibrcom	⊢ ( 𝑊 ∈ LMod → ( 𝑉 = 𝐾 → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) )
17	9 16	syld	⊢ ( 𝑊 ∈ LMod → ( + = · → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) ) )
18	17	imp	⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) )