MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lindfrn Structured version   Visualization version   GIF version

Theorem lindfrn 20283
Description: The range of an independent family is an independent set. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Assertion
Ref Expression
lindfrn ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ∈ (LIndS‘𝑊))

Proof of Theorem lindfrn
Dummy variables 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2724 . . . . 5 (Base‘𝑊) = (Base‘𝑊)
21lindff 20277 . . . 4 ((𝐹 LIndF 𝑊𝑊 ∈ LMod) → 𝐹:dom 𝐹⟶(Base‘𝑊))
32ancoms 468 . . 3 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹:dom 𝐹⟶(Base‘𝑊))
4 frn 6166 . . 3 (𝐹:dom 𝐹⟶(Base‘𝑊) → ran 𝐹 ⊆ (Base‘𝑊))
53, 4syl 17 . 2 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ⊆ (Base‘𝑊))
6 simpll 807 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → 𝑊 ∈ LMod)
7 imassrn 5587 . . . . . . . . 9 (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ ran 𝐹
87, 5syl5ss 3720 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊))
98adantr 472 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊))
10 ffun 6161 . . . . . . . . 9 (𝐹:dom 𝐹⟶(Base‘𝑊) → Fun 𝐹)
113, 10syl 17 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → Fun 𝐹)
12 eldifsn 4425 . . . . . . . . . 10 (𝑥 ∈ (ran 𝐹 ∖ {(𝐹𝑦)}) ↔ (𝑥 ∈ ran 𝐹𝑥 ≠ (𝐹𝑦)))
13 funfn 6031 . . . . . . . . . . . . . 14 (Fun 𝐹𝐹 Fn dom 𝐹)
14 fvelrnb 6357 . . . . . . . . . . . . . 14 (𝐹 Fn dom 𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥))
1513, 14sylbi 207 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥))
1615adantr 472 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥))
17 difss 3845 . . . . . . . . . . . . . . . . . 18 (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹
1817jctr 566 . . . . . . . . . . . . . . . . 17 (Fun 𝐹 → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹))
1918ad2antrr 764 . . . . . . . . . . . . . . . 16 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦))) → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹))
20 simpl 474 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦)) → 𝑘 ∈ dom 𝐹)
21 fveq2 6304 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
2221necon3i 2928 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑘) ≠ (𝐹𝑦) → 𝑘𝑦)
2322adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦)) → 𝑘𝑦)
24 eldifsn 4425 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) ↔ (𝑘 ∈ dom 𝐹𝑘𝑦))
2520, 23, 24sylanbrc 701 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦)) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦}))
2625adantl 473 . . . . . . . . . . . . . . . 16 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦))) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦}))
27 funfvima2 6608 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹) → (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
2819, 26, 27sylc 65 . . . . . . . . . . . . . . 15 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦))) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))
2928expr 644 . . . . . . . . . . . . . 14 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹𝑘) ≠ (𝐹𝑦) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
30 neeq1 2958 . . . . . . . . . . . . . . 15 ((𝐹𝑘) = 𝑥 → ((𝐹𝑘) ≠ (𝐹𝑦) ↔ 𝑥 ≠ (𝐹𝑦)))
31 eleq1 2791 . . . . . . . . . . . . . . 15 ((𝐹𝑘) = 𝑥 → ((𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ↔ 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
3230, 31imbi12d 333 . . . . . . . . . . . . . 14 ((𝐹𝑘) = 𝑥 → (((𝐹𝑘) ≠ (𝐹𝑦) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) ↔ (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3329, 32syl5ibcom 235 . . . . . . . . . . . . 13 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹𝑘) = 𝑥 → (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3433rexlimdva 3133 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥 → (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3516, 34sylbid 230 . . . . . . . . . . 11 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 → (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3635impd 446 . . . . . . . . . 10 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝑥 ∈ ran 𝐹𝑥 ≠ (𝐹𝑦)) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
3712, 36syl5bi 232 . . . . . . . . 9 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝑥 ∈ (ran 𝐹 ∖ {(𝐹𝑦)}) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
3837ssrdv 3715 . . . . . . . 8 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦})))
3911, 38sylan 489 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦})))
40 eqid 2724 . . . . . . . 8 (LSpan‘𝑊) = (LSpan‘𝑊)
411, 40lspss 19107 . . . . . . 7 ((𝑊 ∈ LMod ∧ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊) ∧ (ran 𝐹 ∖ {(𝐹𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
426, 9, 39, 41syl3anc 1439 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
4342adantrr 755 . . . . 5 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
44 simplr 809 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝐹 LIndF 𝑊)
45 simprl 811 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑦 ∈ dom 𝐹)
46 eldifi 3840 . . . . . . 7 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
4746ad2antll 767 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
48 eldifsni 4429 . . . . . . 7 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → 𝑘 ≠ (0g‘(Scalar‘𝑊)))
4948ad2antll 767 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑘 ≠ (0g‘(Scalar‘𝑊)))
50 eqid 2724 . . . . . . 7 ( ·𝑠𝑊) = ( ·𝑠𝑊)
51 eqid 2724 . . . . . . 7 (Scalar‘𝑊) = (Scalar‘𝑊)
52 eqid 2724 . . . . . . 7 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
53 eqid 2724 . . . . . . 7 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
5450, 40, 51, 52, 53lindfind 20278 . . . . . 6 (((𝐹 LIndF 𝑊𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊)))) → ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
5544, 45, 47, 49, 54syl22anc 1440 . . . . 5 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
5643, 55ssneldd 3712 . . . 4 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})))
5756ralrimivva 3073 . . 3 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})))
5811, 13sylib 208 . . . 4 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹 Fn dom 𝐹)
59 oveq2 6773 . . . . . . . 8 (𝑥 = (𝐹𝑦) → (𝑘( ·𝑠𝑊)𝑥) = (𝑘( ·𝑠𝑊)(𝐹𝑦)))
60 sneq 4295 . . . . . . . . . 10 (𝑥 = (𝐹𝑦) → {𝑥} = {(𝐹𝑦)})
6160difeq2d 3836 . . . . . . . . 9 (𝑥 = (𝐹𝑦) → (ran 𝐹 ∖ {𝑥}) = (ran 𝐹 ∖ {(𝐹𝑦)}))
6261fveq2d 6308 . . . . . . . 8 (𝑥 = (𝐹𝑦) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) = ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})))
6359, 62eleq12d 2797 . . . . . . 7 (𝑥 = (𝐹𝑦) → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6463notbid 307 . . . . . 6 (𝑥 = (𝐹𝑦) → (¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6564ralbidv 3088 . . . . 5 (𝑥 = (𝐹𝑦) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6665ralrn 6477 . . . 4 (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6758, 66syl 17 . . 3 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6857, 67mpbird 247 . 2 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})))
691, 50, 40, 51, 53, 52islinds2 20275 . . 3 (𝑊 ∈ LMod → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})))))
7069adantr 472 . 2 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})))))
715, 68, 70mpbir2and 995 1 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ∈ (LIndS‘𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1596  wcel 2103  wne 2896  wral 3014  wrex 3015  cdif 3677  wss 3680  {csn 4285   class class class wbr 4760  dom cdm 5218  ran crn 5219  cima 5221  Fun wfun 5995   Fn wfn 5996  wf 5997  cfv 6001  (class class class)co 6765  Basecbs 15980  Scalarcsca 16067   ·𝑠 cvsca 16068  0gc0g 16223  LModclmod 18986  LSpanclspn 19094   LIndF clindf 20266  LIndSclinds 20267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-slot 15984  df-base 15986  df-0g 16225  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-grp 17547  df-lmod 18988  df-lss 19056  df-lsp 19095  df-lindf 20268  df-linds 20269
This theorem is referenced by:  islindf3  20288  lindsmm  20290  matunitlindflem2  33638
  Copyright terms: Public domain W3C validator