This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ 𝑉 ) )