| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl3 1193 | . 2
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) | 
| 2 |  | drngring 20737 | . . . . . . 7
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | 
| 3 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) | 
| 4 | 3 | frlmlmod 21770 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod) | 
| 5 | 2, 4 | sylan 580 | . . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod) | 
| 6 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(𝑅
freeLMod 𝐼)) =
(Base‘(𝑅 freeLMod
𝐼)) | 
| 7 | 6 | linds1 21831 | . . . . . 6
⊢ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) → 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 8 |  | eqid 2736 | . . . . . . 7
⊢
(LSpan‘(𝑅
freeLMod 𝐼)) =
(LSpan‘(𝑅 freeLMod
𝐼)) | 
| 9 | 6, 8 | lspssv 20982 | . . . . . 6
⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 10 | 5, 7, 9 | syl2an 596 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 11 | 10 | 3impa 1109 | . . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 12 | 11 | adantr 480 | . . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 13 |  | bren2 9024 | . . . . . . 7
⊢ (𝑋 ≈ 𝐼 ↔ (𝑋 ≼ 𝐼 ∧ ¬ 𝑋 ≺ 𝐼)) | 
| 14 | 13 | simprbi 496 | . . . . . 6
⊢ (𝑋 ≈ 𝐼 → ¬ 𝑋 ≺ 𝐼) | 
| 15 |  | snfi 9084 | . . . . . . . . . . . 12
⊢ {𝑦} ∈ Fin | 
| 16 |  | simp2 1137 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝐼 ∈ Fin) | 
| 17 |  | lindsdom 37622 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼) | 
| 18 |  | domfi 9230 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ Fin ∧ 𝑋 ≼ 𝐼) → 𝑋 ∈ Fin) | 
| 19 | 16, 17, 18 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ∈ Fin) | 
| 20 |  | unfi 9212 | . . . . . . . . . . . 12
⊢ (({𝑦} ∈ Fin ∧ 𝑋 ∈ Fin) → ({𝑦} ∪ 𝑋) ∈ Fin) | 
| 21 | 15, 19, 20 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ({𝑦} ∪ 𝑋) ∈ Fin) | 
| 22 | 21 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ({𝑦} ∪ 𝑋) ∈ Fin) | 
| 23 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V | 
| 24 | 23 | snss 4784 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 ↔ {𝑦} ⊆ 𝑋) | 
| 25 | 6, 8 | lspssid 20984 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 26 | 5, 7, 25 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 27 | 26 | 3impa 1109 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 28 | 27 | sseld 3981 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 29 | 24, 28 | biimtrrid 243 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ({𝑦} ⊆ 𝑋 → 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 30 | 29 | con3dimp 408 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ¬ {𝑦} ⊆ 𝑋) | 
| 31 |  | nsspssun 4267 | . . . . . . . . . . 11
⊢ (¬
{𝑦} ⊆ 𝑋 ↔ 𝑋 ⊊ ({𝑦} ∪ 𝑋)) | 
| 32 | 30, 31 | sylib 218 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → 𝑋 ⊊ ({𝑦} ∪ 𝑋)) | 
| 33 |  | php3 9250 | . . . . . . . . . 10
⊢ ((({𝑦} ∪ 𝑋) ∈ Fin ∧ 𝑋 ⊊ ({𝑦} ∪ 𝑋)) → 𝑋 ≺ ({𝑦} ∪ 𝑋)) | 
| 34 | 22, 32, 33 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → 𝑋 ≺ ({𝑦} ∪ 𝑋)) | 
| 35 | 34 | adantrl 716 | . . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → 𝑋 ≺ ({𝑦} ∪ 𝑋)) | 
| 36 |  | simpl1 1191 | . . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → 𝑅 ∈ DivRing) | 
| 37 |  | simpl2 1192 | . . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → 𝐼 ∈ Fin) | 
| 38 |  | snssi 4807 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) → {𝑦} ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → {𝑦} ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 40 | 7 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 41 |  | unss 4189 | . . . . . . . . . . . 12
⊢ (({𝑦} ⊆ (Base‘(𝑅 freeLMod 𝐼)) ∧ 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) ↔ ({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 42 | 41 | biimpi 216 | . . . . . . . . . . 11
⊢ (({𝑦} ⊆ (Base‘(𝑅 freeLMod 𝐼)) ∧ 𝑋 ⊆ (Base‘(𝑅 freeLMod 𝐼))) → ({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 43 | 39, 40, 42 | syl2anr 597 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → ({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 44 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 45 | 28 | con3dimp 408 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ¬ 𝑦 ∈ 𝑋) | 
| 46 |  | difsn 4797 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑦 ∈ 𝑋 → (𝑋 ∖ {𝑦}) = 𝑋) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → (𝑋 ∖ {𝑦}) = 𝑋) | 
| 48 | 47 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) = ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 49 | 44, 48 | neleqtrrd 2863 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) | 
| 50 | 49 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) | 
| 51 |  | difsnid 4809 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑋 → ((𝑋 ∖ {𝑧}) ∪ {𝑧}) = 𝑋) | 
| 52 | 51 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑋 → ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧})) = ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 53 | 52 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑋 → (𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧})) ↔ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 54 | 53 | notbid 318 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑋 → (¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧})) ↔ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 55 | 54 | biimparc 479 | . . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑦 ∈
((LSpan‘(𝑅 freeLMod
𝐼))‘𝑋) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧}))) | 
| 56 | 55 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧}))) | 
| 57 | 3 | frlmsca 21774 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼))) | 
| 58 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈
DivRing) | 
| 59 | 57, 58 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(Scalar‘(𝑅 freeLMod
𝐼)) ∈
DivRing) | 
| 60 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(Scalar‘(𝑅
freeLMod 𝐼)) =
(Scalar‘(𝑅 freeLMod
𝐼)) | 
| 61 | 60 | islvec 21104 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 freeLMod 𝐼) ∈ LVec ↔ ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ DivRing)) | 
| 62 | 5, 59, 61 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LVec) | 
| 63 | 62 | 3adant3 1132 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑅 freeLMod 𝐼) ∈ LVec) | 
| 64 | 63 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → (𝑅 freeLMod 𝐼) ∈ LVec) | 
| 65 | 7 | ssdifssd 4146 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) → (𝑋 ∖ {𝑧}) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 66 | 65 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑋 ∖ {𝑧}) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 67 | 66 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → (𝑋 ∖ {𝑧}) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 68 |  | simp-4r 783 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) | 
| 69 |  | difundir 4290 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝑦} ∪ 𝑋) ∖ {𝑧}) = (({𝑦} ∖ {𝑧}) ∪ (𝑋 ∖ {𝑧})) | 
| 70 | 69 | equncomi 4159 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (({𝑦} ∪ 𝑋) ∖ {𝑧}) = ((𝑋 ∖ {𝑧}) ∪ ({𝑦} ∖ {𝑧})) | 
| 71 |  | elsni 4642 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ {𝑦} → 𝑧 = 𝑦) | 
| 72 | 71 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ {𝑦} → (𝑧 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋)) | 
| 73 | 72 | notbid 318 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ {𝑦} → (¬ 𝑧 ∈ 𝑋 ↔ ¬ 𝑦 ∈ 𝑋)) | 
| 74 | 45, 73 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → (𝑧 ∈ {𝑦} → ¬ 𝑧 ∈ 𝑋)) | 
| 75 | 74 | con2d 134 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → (𝑧 ∈ 𝑋 → ¬ 𝑧 ∈ {𝑦})) | 
| 76 | 75 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑧 ∈ {𝑦}) | 
| 77 |  | difsn 4797 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑧 ∈ {𝑦} → ({𝑦} ∖ {𝑧}) = {𝑦}) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → ({𝑦} ∖ {𝑧}) = {𝑦}) | 
| 79 | 78 | uneq2d 4167 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → ((𝑋 ∖ {𝑧}) ∪ ({𝑦} ∖ {𝑧})) = ((𝑋 ∖ {𝑧}) ∪ {𝑦})) | 
| 80 | 70, 79 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → (({𝑦} ∪ 𝑋) ∖ {𝑧}) = ((𝑋 ∖ {𝑧}) ∪ {𝑦})) | 
| 81 | 80 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) = ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑦}))) | 
| 82 | 81 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑦})))) | 
| 83 | 82 | adantllr 719 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑦})))) | 
| 84 | 83 | biimpa 476 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑦}))) | 
| 85 |  | drngnzr 20749 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) | 
| 86 | 85 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing) | 
| 87 | 57, 86 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) →
(Scalar‘(𝑅 freeLMod
𝐼)) ∈
NzRing) | 
| 88 | 5, 87 | jca 511 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)) | 
| 89 | 88 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))) | 
| 90 | 89 | 3impa 1109 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))) | 
| 91 | 8, 60 | lindsind2 21840 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑧}))) | 
| 92 | 91 | 3expa 1118 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑅 freeLMod
𝐼) ∈ LMod ∧
(Scalar‘(𝑅 freeLMod
𝐼)) ∈ NzRing) ∧
𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑧}))) | 
| 93 | 90, 92 | sylan 580 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑧}))) | 
| 94 | 93 | ad5ant14 757 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑧}))) | 
| 95 | 84, 94 | eldifd 3961 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → 𝑧 ∈ (((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑦})) ∖ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑧})))) | 
| 96 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(LSubSp‘(𝑅
freeLMod 𝐼)) =
(LSubSp‘(𝑅 freeLMod
𝐼)) | 
| 97 | 6, 96, 8 | lspsolv 21146 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 freeLMod 𝐼) ∈ LVec ∧ ((𝑋 ∖ {𝑧}) ⊆ (Base‘(𝑅 freeLMod 𝐼)) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ 𝑧 ∈ (((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑦})) ∖ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑧}))))) → 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧}))) | 
| 98 | 64, 67, 68, 95, 97 | syl13anc 1373 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) → 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘((𝑋 ∖ {𝑧}) ∪ {𝑧}))) | 
| 99 | 56, 98 | mtand 815 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ∧ 𝑧 ∈ 𝑋) → ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) | 
| 100 | 99 | ralrimiva 3145 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ∀𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) | 
| 101 |  | ralunb 4196 | . . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
({𝑦} ∪ 𝑋) ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ (∀𝑧 ∈ {𝑦} ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∧ ∀𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 102 |  | id 22 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) | 
| 103 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑦 → {𝑧} = {𝑦}) | 
| 104 | 103 | difeq2d 4125 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑦 → (({𝑦} ∪ 𝑋) ∖ {𝑧}) = (({𝑦} ∪ 𝑋) ∖ {𝑦})) | 
| 105 |  | uncom 4157 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑦} ∪ 𝑋) = (𝑋 ∪ {𝑦}) | 
| 106 | 105 | difeq1i 4121 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (({𝑦} ∪ 𝑋) ∖ {𝑦}) = ((𝑋 ∪ {𝑦}) ∖ {𝑦}) | 
| 107 |  | difun2 4480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∪ {𝑦}) ∖ {𝑦}) = (𝑋 ∖ {𝑦}) | 
| 108 | 106, 107 | eqtri 2764 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (({𝑦} ∪ 𝑋) ∖ {𝑦}) = (𝑋 ∖ {𝑦}) | 
| 109 | 104, 108 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑦 → (({𝑦} ∪ 𝑋) ∖ {𝑧}) = (𝑋 ∖ {𝑦})) | 
| 110 | 109 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑦 → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) = ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) | 
| 111 | 102, 110 | eleq12d 2834 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑦 → (𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})))) | 
| 112 | 111 | notbid 318 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → (¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})))) | 
| 113 | 23, 112 | ralsn 4680 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
{𝑦} ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦}))) | 
| 114 | 113 | anbi1i 624 | . . . . . . . . . . . . . . 15
⊢
((∀𝑧 ∈
{𝑦} ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∧ ∀𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) ↔ (¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) ∧ ∀𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 115 | 101, 114 | bitri 275 | . . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
({𝑦} ∪ 𝑋) ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ (¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(𝑋 ∖ {𝑦})) ∧ ∀𝑧 ∈ 𝑋 ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 116 | 50, 100, 115 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) → ∀𝑧 ∈ ({𝑦} ∪ 𝑋) ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) | 
| 117 | 116 | ex 412 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → (¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) → ∀𝑧 ∈ ({𝑦} ∪ 𝑋) ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 118 | 63 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (𝑅 freeLMod 𝐼) ∈ LVec) | 
| 119 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈
((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ↔ (𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∧ 𝑥 ≠
(0g‘(Scalar‘(𝑅 freeLMod 𝐼))))) | 
| 120 | 119 | biimpi 216 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈
((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) → (𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∧ 𝑥 ≠
(0g‘(Scalar‘(𝑅 freeLMod 𝐼))))) | 
| 121 | 120 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∧ 𝑥 ≠
(0g‘(Scalar‘(𝑅 freeLMod 𝐼))))) | 
| 122 | 38, 7, 42 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → ({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 123 | 122 | 3ad2antl3 1187 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → ({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 124 | 123 | sselda 3982 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) → 𝑧 ∈ (Base‘(𝑅 freeLMod 𝐼))) | 
| 125 | 124 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → 𝑧 ∈ (Base‘(𝑅 freeLMod 𝐼))) | 
| 126 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢ (
·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠
‘(𝑅 freeLMod 𝐼)) | 
| 127 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) | 
| 128 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘(Scalar‘(𝑅 freeLMod 𝐼))) =
(0g‘(Scalar‘(𝑅 freeLMod 𝐼))) | 
| 129 | 6, 60, 126, 127, 128, 8 | lspsnvs 21117 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 freeLMod 𝐼) ∈ LVec ∧ (𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∧ 𝑥 ≠
(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))) ∧ 𝑧 ∈ (Base‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘{(𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧)}) = ((LSpan‘(𝑅 freeLMod 𝐼))‘{𝑧})) | 
| 130 | 118, 121,
125, 129 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → ((LSpan‘(𝑅 freeLMod 𝐼))‘{(𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧)}) = ((LSpan‘(𝑅 freeLMod 𝐼))‘{𝑧})) | 
| 131 | 130 | sseq1d 4014 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (((LSpan‘(𝑅 freeLMod 𝐼))‘{(𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧)}) ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ((LSpan‘(𝑅 freeLMod 𝐼))‘{𝑧}) ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 132 | 5 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → (𝑅 freeLMod 𝐼) ∈ LMod) | 
| 133 | 132 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (𝑅 freeLMod 𝐼) ∈ LMod) | 
| 134 |  | df-3an 1088 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ↔ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))) | 
| 135 | 122 | ssdifssd 4146 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → (({𝑦} ∪ 𝑋) ∖ {𝑧}) ⊆ (Base‘(𝑅 freeLMod 𝐼))) | 
| 136 | 6, 96, 8 | lspcl 20975 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (({𝑦} ∪ 𝑋) ∖ {𝑧}) ⊆ (Base‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∈ (LSubSp‘(𝑅 freeLMod 𝐼))) | 
| 137 | 5, 135, 136 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∈ (LSubSp‘(𝑅 freeLMod 𝐼))) | 
| 138 | 137 | anassrs 467 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∈ (LSubSp‘(𝑅 freeLMod 𝐼))) | 
| 139 | 134, 138 | sylanb 581 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∈ (LSubSp‘(𝑅 freeLMod 𝐼))) | 
| 140 | 139 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∈ (LSubSp‘(𝑅 freeLMod 𝐼))) | 
| 141 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈
((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) → 𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → 𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))) | 
| 143 | 6, 60, 126, 127 | lmodvscl 20877 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ (Base‘(𝑅 freeLMod 𝐼))) → (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ (Base‘(𝑅 freeLMod 𝐼))) | 
| 144 | 133, 142,
125, 143 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ (Base‘(𝑅 freeLMod 𝐼))) | 
| 145 | 6, 96, 8, 133, 140, 144 | ellspsn5b 20994 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → ((𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ((LSpan‘(𝑅 freeLMod 𝐼))‘{(𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧)}) ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 146 | 132 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) → (𝑅 freeLMod 𝐼) ∈ LMod) | 
| 147 | 139 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ∈ (LSubSp‘(𝑅 freeLMod 𝐼))) | 
| 148 | 6, 96, 8, 146, 147, 124 | ellspsn5b 20994 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) → (𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ((LSpan‘(𝑅 freeLMod 𝐼))‘{𝑧}) ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 149 | 148 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ((LSpan‘(𝑅 freeLMod 𝐼))‘{𝑧}) ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 150 | 131, 145,
149 | 3bitr4rd 312 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 151 | 150 | notbid 318 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) ↔ ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 152 | 151 | biimpd 229 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
DivRing ∧ 𝐼 ∈ Fin
∧ 𝑋 ∈
(LIndS‘(𝑅 freeLMod
𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) ∧ 𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))})) → (¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) → ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 153 | 152 | ralrimdva 3153 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) ∧ 𝑧 ∈ ({𝑦} ∪ 𝑋)) → (¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) → ∀𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 154 | 153 | ralimdva 3166 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → (∀𝑧 ∈ ({𝑦} ∪ 𝑋) ¬ 𝑧 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})) → ∀𝑧 ∈ ({𝑦} ∪ 𝑋)∀𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 155 | 117, 154 | syld 47 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼))) → (¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) → ∀𝑧 ∈ ({𝑦} ∪ 𝑋)∀𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 156 | 155 | impr 454 | . . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → ∀𝑧 ∈ ({𝑦} ∪ 𝑋)∀𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))) | 
| 157 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑅 freeLMod 𝐼) ∈ V | 
| 158 | 6, 126, 8, 60, 127, 128 | islinds2 21834 | . . . . . . . . . . 11
⊢ ((𝑅 freeLMod 𝐼) ∈ V → (({𝑦} ∪ 𝑋) ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ↔ (({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼)) ∧ ∀𝑧 ∈ ({𝑦} ∪ 𝑋)∀𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧}))))) | 
| 159 | 157, 158 | ax-mp 5 | . . . . . . . . . 10
⊢ (({𝑦} ∪ 𝑋) ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ↔ (({𝑦} ∪ 𝑋) ⊆ (Base‘(𝑅 freeLMod 𝐼)) ∧ ∀𝑧 ∈ ({𝑦} ∪ 𝑋)∀𝑥 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod 𝐼)))}) ¬ (𝑥( ·𝑠
‘(𝑅 freeLMod 𝐼))𝑧) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(({𝑦} ∪ 𝑋) ∖ {𝑧})))) | 
| 160 | 43, 156, 159 | sylanbrc 583 | . . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → ({𝑦} ∪ 𝑋) ∈ (LIndS‘(𝑅 freeLMod 𝐼))) | 
| 161 |  | lindsdom 37622 | . . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ({𝑦} ∪ 𝑋) ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → ({𝑦} ∪ 𝑋) ≼ 𝐼) | 
| 162 | 36, 37, 160, 161 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → ({𝑦} ∪ 𝑋) ≼ 𝐼) | 
| 163 |  | sdomdomtr 9151 | . . . . . . . 8
⊢ ((𝑋 ≺ ({𝑦} ∪ 𝑋) ∧ ({𝑦} ∪ 𝑋) ≼ 𝐼) → 𝑋 ≺ 𝐼) | 
| 164 | 35, 162, 163 | syl2anc 584 | . . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) → 𝑋 ≺ 𝐼) | 
| 165 | 164 | stoic1a 1771 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ¬ 𝑋 ≺ 𝐼) → ¬ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 166 | 14, 165 | sylan2 593 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → ¬ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 167 |  | iman 401 | . . . . 5
⊢ ((𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) → 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) ↔ ¬ (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) ∧ ¬ 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 168 | 166, 167 | sylibr 234 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → (𝑦 ∈ (Base‘(𝑅 freeLMod 𝐼)) → 𝑦 ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋))) | 
| 169 | 168 | ssrdv 3988 | . . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → (Base‘(𝑅 freeLMod 𝐼)) ⊆ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋)) | 
| 170 | 12, 169 | eqssd 4000 | . 2
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) = (Base‘(𝑅 freeLMod 𝐼))) | 
| 171 |  | eqid 2736 | . . 3
⊢
(LBasis‘(𝑅
freeLMod 𝐼)) =
(LBasis‘(𝑅 freeLMod
𝐼)) | 
| 172 | 6, 171, 8 | islbs4 21853 | . 2
⊢ (𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼)) ↔ (𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼)) ∧ ((LSpan‘(𝑅 freeLMod 𝐼))‘𝑋) = (Base‘(𝑅 freeLMod 𝐼)))) | 
| 173 | 1, 170, 172 | sylanbrc 583 | 1
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → 𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼))) |