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

Theorem lindfrn 20436
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 2765 . . . . 5 (Base‘𝑊) = (Base‘𝑊)
21lindff 20430 . . . 4 ((𝐹 LIndF 𝑊𝑊 ∈ LMod) → 𝐹:dom 𝐹⟶(Base‘𝑊))
32ancoms 450 . . 3 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹:dom 𝐹⟶(Base‘𝑊))
43frnd 6230 . 2 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ⊆ (Base‘𝑊))
5 simpll 783 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → 𝑊 ∈ LMod)
6 imassrn 5659 . . . . . . . . 9 (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ ran 𝐹
76, 4syl5ss 3772 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊))
87adantr 472 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊))
93ffund 6227 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → Fun 𝐹)
10 eldifsn 4472 . . . . . . . . . 10 (𝑥 ∈ (ran 𝐹 ∖ {(𝐹𝑦)}) ↔ (𝑥 ∈ ran 𝐹𝑥 ≠ (𝐹𝑦)))
11 funfn 6098 . . . . . . . . . . . . . 14 (Fun 𝐹𝐹 Fn dom 𝐹)
12 fvelrnb 6432 . . . . . . . . . . . . . 14 (𝐹 Fn dom 𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥))
1311, 12sylbi 208 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥))
1413adantr 472 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥))
15 difss 3899 . . . . . . . . . . . . . . . . . 18 (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹
1615jctr 520 . . . . . . . . . . . . . . . . 17 (Fun 𝐹 → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹))
1716ad2antrr 717 . . . . . . . . . . . . . . . 16 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦))) → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹))
18 simpl 474 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦)) → 𝑘 ∈ dom 𝐹)
19 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
2019necon3i 2969 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑘) ≠ (𝐹𝑦) → 𝑘𝑦)
2120adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦)) → 𝑘𝑦)
22 eldifsn 4472 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) ↔ (𝑘 ∈ dom 𝐹𝑘𝑦))
2318, 21, 22sylanbrc 578 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦)) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦}))
2423adantl 473 . . . . . . . . . . . . . . . 16 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦))) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦}))
25 funfvima2 6686 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹) → (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
2617, 24, 25sylc 65 . . . . . . . . . . . . . . 15 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ≠ (𝐹𝑦))) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))
2726expr 448 . . . . . . . . . . . . . 14 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹𝑘) ≠ (𝐹𝑦) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
28 neeq1 2999 . . . . . . . . . . . . . . 15 ((𝐹𝑘) = 𝑥 → ((𝐹𝑘) ≠ (𝐹𝑦) ↔ 𝑥 ≠ (𝐹𝑦)))
29 eleq1 2832 . . . . . . . . . . . . . . 15 ((𝐹𝑘) = 𝑥 → ((𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ↔ 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
3028, 29imbi12d 335 . . . . . . . . . . . . . 14 ((𝐹𝑘) = 𝑥 → (((𝐹𝑘) ≠ (𝐹𝑦) → (𝐹𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) ↔ (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3127, 30syl5ibcom 236 . . . . . . . . . . . . 13 (((Fun 𝐹𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹𝑘) = 𝑥 → (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3231rexlimdva 3178 . . . . . . . . . . . 12 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (∃𝑘 ∈ dom 𝐹(𝐹𝑘) = 𝑥 → (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3314, 32sylbid 231 . . . . . . . . . . 11 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 → (𝑥 ≠ (𝐹𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))))
3433impd 398 . . . . . . . . . 10 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝑥 ∈ ran 𝐹𝑥 ≠ (𝐹𝑦)) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
3510, 34syl5bi 233 . . . . . . . . 9 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (𝑥 ∈ (ran 𝐹 ∖ {(𝐹𝑦)}) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))
3635ssrdv 3767 . . . . . . . 8 ((Fun 𝐹𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦})))
379, 36sylan 575 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦})))
38 eqid 2765 . . . . . . . 8 (LSpan‘𝑊) = (LSpan‘𝑊)
391, 38lspss 19256 . . . . . . 7 ((𝑊 ∈ LMod ∧ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊) ∧ (ran 𝐹 ∖ {(𝐹𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
405, 8, 37, 39syl3anc 1490 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
4140adantrr 708 . . . . 5 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
42 simplr 785 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝐹 LIndF 𝑊)
43 simprl 787 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑦 ∈ dom 𝐹)
44 eldifi 3894 . . . . . . 7 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
4544ad2antll 720 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
46 eldifsni 4476 . . . . . . 7 (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) → 𝑘 ≠ (0g‘(Scalar‘𝑊)))
4746ad2antll 720 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → 𝑘 ≠ (0g‘(Scalar‘𝑊)))
48 eqid 2765 . . . . . . 7 ( ·𝑠𝑊) = ( ·𝑠𝑊)
49 eqid 2765 . . . . . . 7 (Scalar‘𝑊) = (Scalar‘𝑊)
50 eqid 2765 . . . . . . 7 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
51 eqid 2765 . . . . . . 7 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
5248, 38, 49, 50, 51lindfind 20431 . . . . . 6 (((𝐹 LIndF 𝑊𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊)))) → ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
5342, 43, 45, 47, 52syl22anc 867 . . . . 5 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦}))))
5441, 53ssneldd 3764 . . . 4 (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})))
5554ralrimivva 3118 . . 3 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})))
569, 11sylib 209 . . . 4 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹 Fn dom 𝐹)
57 oveq2 6850 . . . . . . . 8 (𝑥 = (𝐹𝑦) → (𝑘( ·𝑠𝑊)𝑥) = (𝑘( ·𝑠𝑊)(𝐹𝑦)))
58 sneq 4344 . . . . . . . . . 10 (𝑥 = (𝐹𝑦) → {𝑥} = {(𝐹𝑦)})
5958difeq2d 3890 . . . . . . . . 9 (𝑥 = (𝐹𝑦) → (ran 𝐹 ∖ {𝑥}) = (ran 𝐹 ∖ {(𝐹𝑦)}))
6059fveq2d 6379 . . . . . . . 8 (𝑥 = (𝐹𝑦) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) = ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)})))
6157, 60eleq12d 2838 . . . . . . 7 (𝑥 = (𝐹𝑦) → ((𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6261notbid 309 . . . . . 6 (𝑥 = (𝐹𝑦) → (¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6362ralbidv 3133 . . . . 5 (𝑥 = (𝐹𝑦) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6463ralrn 6552 . . . 4 (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6556, 64syl 17 . . 3 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑦 ∈ dom 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)(𝐹𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹𝑦)}))))
6655, 65mpbird 248 . 2 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})))
671, 48, 38, 49, 51, 50islinds2 20428 . . 3 (𝑊 ∈ LMod → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})))))
6867adantr 472 . 2 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})))))
694, 66, 68mpbir2and 704 1 ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ∈ (LIndS‘𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  cdif 3729  wss 3732  {csn 4334   class class class wbr 4809  dom cdm 5277  ran crn 5278  cima 5280  Fun wfun 6062   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  Basecbs 16130  Scalarcsca 16217   ·𝑠 cvsca 16218  0gc0g 16366  LModclmod 19132  LSpanclspn 19243   LIndF clindf 20419  LIndSclinds 20420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-slot 16134  df-base 16136  df-0g 16368  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-grp 17692  df-lmod 19134  df-lss 19202  df-lsp 19244  df-lindf 20421  df-linds 20422
This theorem is referenced by:  islindf3  20441  lindsmm  20443  matunitlindflem2  33830
  Copyright terms: Public domain W3C validator