| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rellindf 21829 | . . . 4
⊢ Rel
LIndF | 
| 2 | 1 | brrelex1i 5740 | . . 3
⊢ (𝐹 LIndF 𝑋 → 𝐹 ∈ V) | 
| 3 | 2 | a1i 11 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → (𝐹 LIndF 𝑋 → 𝐹 ∈ V)) | 
| 4 | 1 | brrelex1i 5740 | . . 3
⊢ (𝐹 LIndF 𝑊 → 𝐹 ∈ V) | 
| 5 | 4 | a1i 11 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → (𝐹 LIndF 𝑊 → 𝐹 ∈ V)) | 
| 6 |  | simpr 484 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹:dom 𝐹⟶(Base‘𝑋)) → 𝐹:dom 𝐹⟶(Base‘𝑋)) | 
| 7 |  | lsslindf.x | . . . . . . . . 9
⊢ 𝑋 = (𝑊 ↾s 𝑆) | 
| 8 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 9 | 7, 8 | ressbasss 17285 | . . . . . . . 8
⊢
(Base‘𝑋)
⊆ (Base‘𝑊) | 
| 10 |  | fss 6751 | . . . . . . . 8
⊢ ((𝐹:dom 𝐹⟶(Base‘𝑋) ∧ (Base‘𝑋) ⊆ (Base‘𝑊)) → 𝐹:dom 𝐹⟶(Base‘𝑊)) | 
| 11 | 6, 9, 10 | sylancl 586 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹:dom 𝐹⟶(Base‘𝑋)) → 𝐹:dom 𝐹⟶(Base‘𝑊)) | 
| 12 |  | ffn 6735 | . . . . . . . . 9
⊢ (𝐹:dom 𝐹⟶(Base‘𝑊) → 𝐹 Fn dom 𝐹) | 
| 13 | 12 | adantl 481 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹:dom 𝐹⟶(Base‘𝑊)) → 𝐹 Fn dom 𝐹) | 
| 14 |  | simp3 1138 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → ran 𝐹 ⊆ 𝑆) | 
| 15 |  | lsslindf.u | . . . . . . . . . . . . 13
⊢ 𝑈 = (LSubSp‘𝑊) | 
| 16 | 8, 15 | lssss 20935 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ 𝑈 → 𝑆 ⊆ (Base‘𝑊)) | 
| 17 | 16 | 3ad2ant2 1134 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → 𝑆 ⊆ (Base‘𝑊)) | 
| 18 | 7, 8 | ressbas2 17284 | . . . . . . . . . . 11
⊢ (𝑆 ⊆ (Base‘𝑊) → 𝑆 = (Base‘𝑋)) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → 𝑆 = (Base‘𝑋)) | 
| 20 | 14, 19 | sseqtrd 4019 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → ran 𝐹 ⊆ (Base‘𝑋)) | 
| 21 | 20 | adantr 480 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹:dom 𝐹⟶(Base‘𝑊)) → ran 𝐹 ⊆ (Base‘𝑋)) | 
| 22 |  | df-f 6564 | . . . . . . . 8
⊢ (𝐹:dom 𝐹⟶(Base‘𝑋) ↔ (𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ (Base‘𝑋))) | 
| 23 | 13, 21, 22 | sylanbrc 583 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹:dom 𝐹⟶(Base‘𝑊)) → 𝐹:dom 𝐹⟶(Base‘𝑋)) | 
| 24 | 11, 23 | impbida 800 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → (𝐹:dom 𝐹⟶(Base‘𝑋) ↔ 𝐹:dom 𝐹⟶(Base‘𝑊))) | 
| 25 | 24 | adantr 480 | . . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (𝐹:dom 𝐹⟶(Base‘𝑋) ↔ 𝐹:dom 𝐹⟶(Base‘𝑊))) | 
| 26 |  | simpl2 1192 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → 𝑆 ∈ 𝑈) | 
| 27 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 28 | 7, 27 | resssca 17388 | . . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑈 → (Scalar‘𝑊) = (Scalar‘𝑋)) | 
| 29 | 28 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝑆 ∈ 𝑈 → (Scalar‘𝑋) = (Scalar‘𝑊)) | 
| 30 | 26, 29 | syl 17 | . . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (Scalar‘𝑋) = (Scalar‘𝑊)) | 
| 31 | 30 | fveq2d 6909 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) →
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑊))) | 
| 32 | 30 | fveq2d 6909 | . . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) →
(0g‘(Scalar‘𝑋)) =
(0g‘(Scalar‘𝑊))) | 
| 33 | 32 | sneqd 4637 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) →
{(0g‘(Scalar‘𝑋))} =
{(0g‘(Scalar‘𝑊))}) | 
| 34 | 31, 33 | difeq12d 4126 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) →
((Base‘(Scalar‘𝑋)) ∖
{(0g‘(Scalar‘𝑋))}) = ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))})) | 
| 35 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 36 | 7, 35 | ressvsca 17389 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ 𝑈 → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) | 
| 37 | 36 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑈 → (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑊)) | 
| 38 | 26, 37 | syl 17 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑊)) | 
| 39 | 38 | oveqd 7449 | . . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) = (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥))) | 
| 40 |  | simpl1 1191 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → 𝑊 ∈ LMod) | 
| 41 |  | imassrn 6088 | . . . . . . . . . . 11
⊢ (𝐹 “ (dom 𝐹 ∖ {𝑥})) ⊆ ran 𝐹 | 
| 42 |  | simpl3 1193 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → ran 𝐹 ⊆ 𝑆) | 
| 43 | 41, 42 | sstrid 3994 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (𝐹 “ (dom 𝐹 ∖ {𝑥})) ⊆ 𝑆) | 
| 44 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) | 
| 45 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(LSpan‘𝑋) =
(LSpan‘𝑋) | 
| 46 | 7, 44, 45, 15 | lsslsp 21014 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ (𝐹 “ (dom 𝐹 ∖ {𝑥})) ⊆ 𝑆) → ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) = ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))) | 
| 47 | 40, 26, 43, 46 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) = ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))) | 
| 48 | 39, 47 | eleq12d 2834 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → ((𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 49 | 48 | notbid 318 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (¬ (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 50 | 34, 49 | raleqbidv 3345 | . . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (∀𝑘 ∈
((Base‘(Scalar‘𝑋)) ∖
{(0g‘(Scalar‘𝑋))}) ¬ (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 51 | 50 | ralbidv 3177 | . . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑋)) ∖
{(0g‘(Scalar‘𝑋))}) ¬ (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 52 | 25, 51 | anbi12d 632 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → ((𝐹:dom 𝐹⟶(Base‘𝑋) ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑋)) ∖
{(0g‘(Scalar‘𝑋))}) ¬ (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹⟶(Base‘𝑊) ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 53 | 7 | ovexi 7466 | . . . . . 6
⊢ 𝑋 ∈ V | 
| 54 | 53 | a1i 11 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → 𝑋 ∈ V) | 
| 55 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑋) =
(Base‘𝑋) | 
| 56 |  | eqid 2736 | . . . . . 6
⊢ (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑋) | 
| 57 |  | eqid 2736 | . . . . . 6
⊢
(Scalar‘𝑋) =
(Scalar‘𝑋) | 
| 58 |  | eqid 2736 | . . . . . 6
⊢
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋)) | 
| 59 |  | eqid 2736 | . . . . . 6
⊢
(0g‘(Scalar‘𝑋)) =
(0g‘(Scalar‘𝑋)) | 
| 60 | 55, 56, 45, 57, 58, 59 | islindf 21833 | . . . . 5
⊢ ((𝑋 ∈ V ∧ 𝐹 ∈ V) → (𝐹 LIndF 𝑋 ↔ (𝐹:dom 𝐹⟶(Base‘𝑋) ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑋)) ∖
{(0g‘(Scalar‘𝑋))}) ¬ (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 61 | 54, 60 | sylan 580 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (𝐹 LIndF 𝑋 ↔ (𝐹:dom 𝐹⟶(Base‘𝑋) ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑋)) ∖
{(0g‘(Scalar‘𝑋))}) ¬ (𝑘( ·𝑠
‘𝑋)(𝐹‘𝑥)) ∈ ((LSpan‘𝑋)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 62 |  | eqid 2736 | . . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 63 |  | eqid 2736 | . . . . . 6
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 64 | 8, 35, 44, 27, 62, 63 | islindf 21833 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐹 ∈ V) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶(Base‘𝑊) ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 65 | 64 | 3ad2antl1 1185 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶(Base‘𝑊) ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑥)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 66 | 52, 61, 65 | 3bitr4d 311 | . . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) ∧ 𝐹 ∈ V) → (𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊)) | 
| 67 | 66 | ex 412 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → (𝐹 ∈ V → (𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊))) | 
| 68 | 3, 5, 67 | pm5.21ndd 379 | 1
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆) → (𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊)) |