Metamath Proof Explorer

Theorem lindsenlbs

Description: A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion lindsenlbs ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → 𝑋 ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) )
2 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3 eqid ⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 )
4 3 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
5 2 4 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
6 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
7 6 linds1 ⊢ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
8 eqid ⊢ ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) )
9 6 8 lspssv ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
10 5 7 9 syl2an ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
11 10 3impa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
12 11 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
13 bren2 ⊢ ( 𝑋 ≈ 𝐼 ↔ ( 𝑋 ≼ 𝐼 ∧ ¬ 𝑋 ≺ 𝐼 ) )
14 13 simprbi ⊢ ( 𝑋 ≈ 𝐼 → ¬ 𝑋 ≺ 𝐼 )
15 snfi ⊢ { 𝑦 } ∈ Fin
16 simp2 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝐼 ∈ Fin )
17 lindsdom ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ≼ 𝐼 )
18 domfi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑋 ≼ 𝐼 ) → 𝑋 ∈ Fin )
19 16 17 18 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ∈ Fin )
20 unfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ 𝑋 ∈ Fin ) → ( { 𝑦 } ∪ 𝑋 ) ∈ Fin )
21 15 19 20 sylancr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ∈ Fin )
22 21 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( { 𝑦 } ∪ 𝑋 ) ∈ Fin )
23 vex ⊢ 𝑦 ∈ V
24 23 snss ⊢ ( 𝑦 ∈ 𝑋 ↔ { 𝑦 } ⊆ 𝑋 )
25 6 8 lspssid ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
26 5 7 25 syl2an ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
27 26 3impa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
28 27 sseld ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑦 ∈ 𝑋 → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
29 24 28 biimtrrid ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ⊆ 𝑋 → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
30 29 con3dimp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ { 𝑦 } ⊆ 𝑋 )
31 nsspssun ⊢ ( ¬ { 𝑦 } ⊆ 𝑋 ↔ 𝑋 ⊊ ( { 𝑦 } ∪ 𝑋 ) )
32 30 31 sylib ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → 𝑋 ⊊ ( { 𝑦 } ∪ 𝑋 ) )
33 php3 ⊢ ( ( ( { 𝑦 } ∪ 𝑋 ) ∈ Fin ∧ 𝑋 ⊊ ( { 𝑦 } ∪ 𝑋 ) ) → 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) )
34 22 32 33 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) )
35 34 adantrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) )
36 simpl1 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝑅 ∈ DivRing )
37 simpl2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝐼 ∈ Fin )
38 snssi ⊢ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
39 38 adantr ⊢ ( ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
40 7 3ad2ant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
41 unss ⊢ ( ( { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
42 41 biimpi ⊢ ( ( { 𝑦 } ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑋 ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
43 39 40 42 syl2anr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
44 simpr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
45 28 con3dimp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ 𝑋 )
46 difsn ⊢ ( ¬ 𝑦 ∈ 𝑋 → ( 𝑋 ∖ { 𝑦 } ) = 𝑋 )
47 45 46 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( 𝑋 ∖ { 𝑦 } ) = 𝑋 )
48 47 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
49 44 48 neleqtrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
50 49 adantlr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
51 difsnid ⊢ ( 𝑧 ∈ 𝑋 → ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝑋 )
52 51 fveq2d ⊢ ( 𝑧 ∈ 𝑋 → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
53 52 eleq2d ⊢ ( 𝑧 ∈ 𝑋 → ( 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) ↔ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
54 53 notbid ⊢ ( 𝑧 ∈ 𝑋 → ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) ↔ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
55 54 biimparc ⊢ ( ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
56 55 adantll ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
57 3 frlmsca ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
58 simpl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ DivRing )
59 57 58 eqeltrrd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ DivRing )
60 eqid ⊢ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) )
61 60 islvec ⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ↔ ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ DivRing ) )
62 5 59 61 sylanbrc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
63 62 3adant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
64 63 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
65 7 ssdifssd ⊢ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
66 65 3ad2ant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
67 66 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
68 simp-4r ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
69 difundir ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( { 𝑦 } ∖ { 𝑧 } ) ∪ ( 𝑋 ∖ { 𝑧 } ) )
70 69 equncomi ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( 𝑋 ∖ { 𝑧 } ) ∪ ( { 𝑦 } ∖ { 𝑧 } ) )
71 elsni ⊢ ( 𝑧 ∈ { 𝑦 } → 𝑧 = 𝑦 )
72 71 eleq1d ⊢ ( 𝑧 ∈ { 𝑦 } → ( 𝑧 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋 ) )
73 72 notbid ⊢ ( 𝑧 ∈ { 𝑦 } → ( ¬ 𝑧 ∈ 𝑋 ↔ ¬ 𝑦 ∈ 𝑋 ) )
74 45 73 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( 𝑧 ∈ { 𝑦 } → ¬ 𝑧 ∈ 𝑋 ) )
75 74 con2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ( 𝑧 ∈ 𝑋 → ¬ 𝑧 ∈ { 𝑦 } ) )
76 75 imp ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ { 𝑦 } )
77 difsn ⊢ ( ¬ 𝑧 ∈ { 𝑦 } → ( { 𝑦 } ∖ { 𝑧 } ) = { 𝑦 } )
78 76 77 syl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( { 𝑦 } ∖ { 𝑧 } ) = { 𝑦 } )
79 78 uneq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑋 ∖ { 𝑧 } ) ∪ ( { 𝑦 } ∖ { 𝑧 } ) ) = ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) )
80 70 79 eqtrid ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) )
81 80 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) )
82 81 eleq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ) )
83 82 adantllr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ) )
84 83 biimpa ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) )
85 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
86 85 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ NzRing )
87 57 86 eqeltrrd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing )
88 5 87 jca ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) → ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) )
89 88 anim1i ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
90 89 3impa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
91 8 60 lindsind2 ⊢ ( ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
92 91 3expa ⊢ ( ( ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ∈ NzRing ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
93 90 92 sylan ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
94 93 ad5ant14 ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) )
95 84 94 eldifd ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑧 ∈ ( ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) ) )
96 eqid ⊢ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) )
97 6 96 8 lspsolv ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ∧ ( ( 𝑋 ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑧 ∈ ( ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑧 } ) ) ) ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
98 64 67 68 95 97 syl13anc ⊢ ( ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( 𝑋 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
99 56 98 mtand ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ∧ 𝑧 ∈ 𝑋 ) → ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
100 99 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
101 ralunb ⊢ ( ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ∀ 𝑧 ∈ { 𝑦 } ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
102 id ⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
103 sneq ⊢ ( 𝑧 = 𝑦 → { 𝑧 } = { 𝑦 } )
104 103 difeq2d ⊢ ( 𝑧 = 𝑦 → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑦 } ) )
105 uncom ⊢ ( { 𝑦 } ∪ 𝑋 ) = ( 𝑋 ∪ { 𝑦 } )
106 105 difeq1i ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑦 } ) = ( ( 𝑋 ∪ { 𝑦 } ) ∖ { 𝑦 } )
107 difun2 ⊢ ( ( 𝑋 ∪ { 𝑦 } ) ∖ { 𝑦 } ) = ( 𝑋 ∖ { 𝑦 } )
108 106 107 eqtri ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑦 } ) = ( 𝑋 ∖ { 𝑦 } )
109 104 108 eqtrdi ⊢ ( 𝑧 = 𝑦 → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) = ( 𝑋 ∖ { 𝑦 } ) )
110 109 fveq2d ⊢ ( 𝑧 = 𝑦 → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
111 102 110 eleq12d ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) )
112 111 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ) )
113 23 112 ralsn ⊢ ( ∀ 𝑧 ∈ { 𝑦 } ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) )
114 113 anbi1i ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 } ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) ↔ ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
115 101 114 bitri ⊢ ( ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( 𝑋 ∖ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
116 50 100 115 sylanbrc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
117 116 ex ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
118 63 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LVec )
119 eldifsn ⊢ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ↔ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) )
120 119 bilani ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) )
121 38 7 42 syl2anr ⊢ ( ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
122 121 3ad2antl3 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
123 122 sselda ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
124 123 adantr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
125 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) )
126 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
127 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) = ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
128 6 60 125 126 127 8 lspsnvs ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LVec ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑥 ≠ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) ∧ 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) )
129 118 120 124 128 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) = ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) )
130 129 sseq1d ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
131 5 3adant3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
132 131 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
133 df-3an ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ↔ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
134 121 ssdifssd ⊢ ( ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
135 6 96 8 lspcl ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
136 5 134 135 syl2an ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
137 136 anassrs ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ) ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
138 133 137 sylanb ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
139 138 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
140 eldifi ⊢ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
141 140 adantl ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
142 6 60 125 126 lmodvscl ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
143 132 141 124 142 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
144 6 96 8 132 139 143 ellspsn5b ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
145 131 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
146 138 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ∈ ( LSubSp ‘ ( 𝑅 freeLMod 𝐼 ) ) )
147 6 96 8 145 146 123 ellspsn5b ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
148 147 adantr ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ { 𝑧 } ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
149 130 144 148 3bitr4rd ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
150 149 notbid ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ↔ ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
151 150 biimpd ⊢ ( ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ) → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) → ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
152 151 ralrimdva ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ) → ( ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) → ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
153 152 ralimdva ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ¬ 𝑧 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
154 117 153 syld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
155 154 impr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) )
156 ovex ⊢ ( 𝑅 freeLMod 𝐼 ) ∈ V
157 6 125 8 60 126 127 islinds2 ⊢ ( ( 𝑅 freeLMod 𝐼 ) ∈ V → ( ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ↔ ( ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) ) )
158 156 157 ax-mp ⊢ ( ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ↔ ( ( { 𝑦 } ∪ 𝑋 ) ⊆ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ∀ 𝑧 ∈ ( { 𝑦 } ∪ 𝑋 ) ∀ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) ) } ) ¬ ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod 𝐼 ) ) 𝑧 ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ ( ( { 𝑦 } ∪ 𝑋 ) ∖ { 𝑧 } ) ) ) )
159 43 155 158 sylanbrc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) )
160 lindsdom ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ( { 𝑦 } ∪ 𝑋 ) ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ≼ 𝐼 )
161 36 37 159 160 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → ( { 𝑦 } ∪ 𝑋 ) ≼ 𝐼 )
162 sdomdomtr ⊢ ( ( 𝑋 ≺ ( { 𝑦 } ∪ 𝑋 ) ∧ ( { 𝑦 } ∪ 𝑋 ) ≼ 𝐼 ) → 𝑋 ≺ 𝐼 )
163 35 161 162 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ) → 𝑋 ≺ 𝐼 )
164 163 stoic1a ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ ¬ 𝑋 ≺ 𝐼 ) → ¬ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
165 14 164 sylan2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ¬ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
166 iman ⊢ ( ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) ↔ ¬ ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ¬ 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
167 165 166 sylibr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑦 ∈ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) ) )
168 167 ssrdv ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ⊆ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) )
169 12 168 eqssd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
170 eqid ⊢ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) )
171 6 170 8 islbs4 ⊢ ( 𝑋 ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) ↔ ( 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ ( ( LSpan ‘ ( 𝑅 freeLMod 𝐼 ) ) ‘ 𝑋 ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) )
172 1 169 171 sylanbrc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ ( LIndS ‘ ( 𝑅 freeLMod 𝐼 ) ) ) ∧ 𝑋 ≈ 𝐼 ) → 𝑋 ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )