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

Metamath Proof Explorer

Theorem islss

Description: The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lssset.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lssset.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
lssset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lssset.p ⊢ + = ( +g ‘ 𝑊 )
lssset.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lssset.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion islss ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lssset.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 lssset.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 lssset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 lssset.p ⊢ + = ( +g ‘ 𝑊 )
5 lssset.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lssset.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
7 elfvex ⊢ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) → 𝑊 ∈ V )
8 7 6 eleq2s ⊢ ( 𝑈 ∈ 𝑆 → 𝑊 ∈ V )
9 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
10 3 9 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝑉 = ∅ )
11 10 sseq2d ⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ⊆ 𝑉 ↔ 𝑈 ⊆ ∅ ) )
12 11 biimpcd ⊢ ( 𝑈 ⊆ 𝑉 → ( ¬ 𝑊 ∈ V → 𝑈 ⊆ ∅ ) )
13 ss0 ⊢ ( 𝑈 ⊆ ∅ → 𝑈 = ∅ )
14 12 13 syl6 ⊢ ( 𝑈 ⊆ 𝑉 → ( ¬ 𝑊 ∈ V → 𝑈 = ∅ ) )
15 14 necon1ad ⊢ ( 𝑈 ⊆ 𝑉 → ( 𝑈 ≠ ∅ → 𝑊 ∈ V ) )
16 15 imp ⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) → 𝑊 ∈ V )
17 16 3adant3 ⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) → 𝑊 ∈ V )
18 1 2 3 4 5 6 lssset ⊢ ( 𝑊 ∈ V → 𝑆 = { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } )
19 18 eleq2d ⊢ ( 𝑊 ∈ V → ( 𝑈 ∈ 𝑆 ↔ 𝑈 ∈ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ) )
20 eldifsn ⊢ ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑈 ∈ 𝒫 𝑉 ∧ 𝑈 ≠ ∅ ) )
21 3 fvexi ⊢ 𝑉 ∈ V
22 21 elpw2 ⊢ ( 𝑈 ∈ 𝒫 𝑉 ↔ 𝑈 ⊆ 𝑉 )
23 22 anbi1i ⊢ ( ( 𝑈 ∈ 𝒫 𝑉 ∧ 𝑈 ≠ ∅ ) ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) )
24 20 23 bitri ⊢ ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) )
25 24 anbi1i ⊢ ( ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ↔ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
26 eleq2 ⊢ ( 𝑠 = 𝑈 → ( ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
27 26 raleqbi1dv ⊢ ( 𝑠 = 𝑈 → ( ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
28 27 raleqbi1dv ⊢ ( 𝑠 = 𝑈 → ( ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
29 28 ralbidv ⊢ ( 𝑠 = 𝑈 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
30 29 elrab ⊢ ( 𝑈 ∈ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ↔ ( 𝑈 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
31 df-3an ⊢ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ↔ ( ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
32 25 30 31 3bitr4i ⊢ ( 𝑈 ∈ { 𝑠 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑠 } ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )
33 19 32 bitrdi ⊢ ( 𝑊 ∈ V → ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) ) )
34 8 17 33 pm5.21nii ⊢ ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ 𝑈 ∀ 𝑏 ∈ 𝑈 ( ( 𝑥 · 𝑎 ) + 𝑏 ) ∈ 𝑈 ) )