Metamath Proof Explorer

Theorem frlmlbs

Description: The unit vectors comprise a basis for a free module. (Contributed by Stefan O'Rear, 6-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmlbs.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmlbs.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
frlmlbs.j ⊢ 𝐽 = ( LBasis ‘ 𝐹 )
Assertion frlmlbs ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran 𝑈 ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 frlmlbs.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmlbs.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
3 frlmlbs.j ⊢ 𝐽 = ( LBasis ‘ 𝐹 )
4 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
5 2 1 4 uvcff ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) )
6 5 frnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran 𝑈 ⊆ ( Base ‘ 𝐹 ) )
7 suppssdm ⊢ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ dom 𝑎
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 1 8 4 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → 𝑎 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
10 9 adantll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → 𝑎 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
11 7 10 fssdm ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 )
12 11 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐹 ) ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 )
13 rabid2 ⊢ ( ( Base ‘ 𝐹 ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐹 ) ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 )
14 12 13 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( Base ‘ 𝐹 ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } )
15 ssid ⊢ 𝐼 ⊆ 𝐼
16 eqid ⊢ ( LSpan ‘ 𝐹 ) = ( LSpan ‘ 𝐹 )
17 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18 eqid ⊢ { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 }
19 1 2 16 4 17 18 frlmsslsp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐼 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ 𝐼 ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } )
20 15 19 mp3an3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ 𝐼 ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } )
21 ffn ⊢ ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) → 𝑈 Fn 𝐼 )
22 fnima ⊢ ( 𝑈 Fn 𝐼 → ( 𝑈 “ 𝐼 ) = ran 𝑈 )
23 5 21 22 3syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝑈 “ 𝐼 ) = ran 𝑈 )
24 23 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ 𝐼 ) ) = ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) )
25 14 20 24 3eqtr2rd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) )
26 eqid ⊢ ( ·𝑠 ‘ 𝐹 ) = ( ·𝑠 ‘ 𝐹 )
27 eqid ⊢ { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) }
28 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑅 ∈ Ring )
29 simplr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝐼 ∈ 𝑉 )
30 difssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝐼 ∖ { 𝑐 } ) ⊆ 𝐼 )
31 vsnid ⊢ 𝑐 ∈ { 𝑐 }
32 snssi ⊢ ( 𝑐 ∈ 𝐼 → { 𝑐 } ⊆ 𝐼 )
33 32 ad2antrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → { 𝑐 } ⊆ 𝐼 )
34 dfss4 ⊢ ( { 𝑐 } ⊆ 𝐼 ↔ ( 𝐼 ∖ ( 𝐼 ∖ { 𝑐 } ) ) = { 𝑐 } )
35 33 34 sylib ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝐼 ∖ ( 𝐼 ∖ { 𝑐 } ) ) = { 𝑐 } )
36 31 35 eleqtrrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑐 ∈ ( 𝐼 ∖ ( 𝐼 ∖ { 𝑐 } ) ) )
37 1 frlmsca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
38 37 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
39 37 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝐹 ) ) )
40 39 sneqd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → { ( 0g ‘ 𝑅 ) } = { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } )
41 38 40 difeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) )
42 41 eleq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ↔ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) )
43 42 biimpar ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
44 43 adantrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
45 1 2 4 8 26 17 27 28 29 30 36 44 frlmssuvc2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
46 17 8 ringelnzr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑅 ∈ NzRing )
47 28 44 46 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑅 ∈ NzRing )
48 2 1 4 uvcf1 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) )
49 47 29 48 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) )
50 df-f1 ⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) ↔ ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) ∧ Fun ◡ 𝑈 ) )
51 50 simprbi ⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) → Fun ◡ 𝑈 )
52 imadif ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) = ( ( 𝑈 “ 𝐼 ) ∖ ( 𝑈 “ { 𝑐 } ) ) )
53 49 51 52 3syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) = ( ( 𝑈 “ 𝐼 ) ∖ ( 𝑈 “ { 𝑐 } ) ) )
54 f1fn ⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) → 𝑈 Fn 𝐼 )
55 49 54 22 3syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝑈 “ 𝐼 ) = ran 𝑈 )
56 49 54 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑈 Fn 𝐼 )
57 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑐 ∈ 𝐼 )
58 fnsnfv ⊢ ( ( 𝑈 Fn 𝐼 ∧ 𝑐 ∈ 𝐼 ) → { ( 𝑈 ‘ 𝑐 ) } = ( 𝑈 “ { 𝑐 } ) )
59 56 57 58 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → { ( 𝑈 ‘ 𝑐 ) } = ( 𝑈 “ { 𝑐 } ) )
60 59 eqcomd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝑈 “ { 𝑐 } ) = { ( 𝑈 ‘ 𝑐 ) } )
61 55 60 difeq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( 𝑈 “ 𝐼 ) ∖ ( 𝑈 “ { 𝑐 } ) ) = ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) )
62 53 61 eqtr2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) = ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) )
63 62 fveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) = ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) ) )
64 1 2 16 4 17 27 frlmsslsp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ ( 𝐼 ∖ { 𝑐 } ) ⊆ 𝐼 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
65 28 29 30 64 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
66 63 65 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
67 45 66 neleqtrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) )
68 67 ralrimivva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑐 ∈ 𝐼 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) )
69 oveq2 ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) = ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) )
70 sneq ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → { 𝑎 } = { ( 𝑈 ‘ 𝑐 ) } )
71 70 difeq2d ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ran 𝑈 ∖ { 𝑎 } ) = ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) )
72 71 fveq2d ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) = ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) )
73 69 72 eleq12d ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
74 73 notbid ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
75 74 ralbidv ⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
76 75 ralrn ⊢ ( 𝑈 Fn 𝐼 → ( ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ∀ 𝑐 ∈ 𝐼 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
77 5 21 76 3syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ∀ 𝑐 ∈ 𝐼 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
78 68 77 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) )
79 1 ovexi ⊢ 𝐹 ∈ V
80 eqid ⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
81 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
82 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐹 ) ) = ( 0g ‘ ( Scalar ‘ 𝐹 ) )
83 4 80 26 81 3 16 82 islbs ⊢ ( 𝐹 ∈ V → ( ran 𝑈 ∈ 𝐽 ↔ ( ran 𝑈 ⊆ ( Base ‘ 𝐹 ) ∧ ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) ∧ ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ) ) )
84 79 83 ax-mp ⊢ ( ran 𝑈 ∈ 𝐽 ↔ ( ran 𝑈 ⊆ ( Base ‘ 𝐹 ) ∧ ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) ∧ ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ) )
85 6 25 78 84 syl3anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran 𝑈 ∈ 𝐽 )