This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rgmoddimOLD

Description: Obsolete version of rlmdim as of 21-Mar-2025. (Contributed by Thierry Arnoux, 5-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rlmdim.1 ⊢ 𝑉 = ( ringLMod ‘ 𝐹 )
Assertion rgmoddimOLD ( 𝐹 ∈ Field → ( dim ‘ 𝑉 ) = 1 )

Proof

Step Hyp Ref Expression
1 rlmdim.1 ⊢ 𝑉 = ( ringLMod ‘ 𝐹 )
2 isfld ⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
3 2 simplbi ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
4 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
5 4 ressid ⊢ ( 𝐹 ∈ Field → ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) = 𝐹 )
6 5 3 eqeltrd ⊢ ( 𝐹 ∈ Field → ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing )
7 drngring ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
8 4 subrgid ⊢ ( 𝐹 ∈ Ring → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) )
9 3 7 8 3syl ⊢ ( 𝐹 ∈ Field → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) )
10 rlmval ⊢ ( ringLMod ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐹 ) )
11 1 10 eqtri ⊢ 𝑉 = ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐹 ) )
12 eqid ⊢ ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) = ( 𝐹 ↾s ( Base ‘ 𝐹 ) )
13 11 12 sralvec ⊢ ( ( 𝐹 ∈ DivRing ∧ ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) ) → 𝑉 ∈ LVec )
14 3 6 9 13 syl3anc ⊢ ( 𝐹 ∈ Field → 𝑉 ∈ LVec )
15 3 7 syl ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ Ring )
16 ssidd ⊢ ( 𝐹 ∈ Field → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐹 ) )
17 11 4 sraring ⊢ ( ( 𝐹 ∈ Ring ∧ ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐹 ) ) → 𝑉 ∈ Ring )
18 15 16 17 syl2anc ⊢ ( 𝐹 ∈ Field → 𝑉 ∈ Ring )
19 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
20 eqid ⊢ ( 1r ‘ 𝑉 ) = ( 1r ‘ 𝑉 )
21 19 20 ringidcl ⊢ ( 𝑉 ∈ Ring → ( 1r ‘ 𝑉 ) ∈ ( Base ‘ 𝑉 ) )
22 18 21 syl ⊢ ( 𝐹 ∈ Field → ( 1r ‘ 𝑉 ) ∈ ( Base ‘ 𝑉 ) )
23 11 4 sradrng ⊢ ( ( 𝐹 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐹 ) ) → 𝑉 ∈ DivRing )
24 3 16 23 syl2anc ⊢ ( 𝐹 ∈ Field → 𝑉 ∈ DivRing )
25 eqid ⊢ ( 0g ‘ 𝑉 ) = ( 0g ‘ 𝑉 )
26 25 20 drngunz ⊢ ( 𝑉 ∈ DivRing → ( 1r ‘ 𝑉 ) ≠ ( 0g ‘ 𝑉 ) )
27 24 26 syl ⊢ ( 𝐹 ∈ Field → ( 1r ‘ 𝑉 ) ≠ ( 0g ‘ 𝑉 ) )
28 19 25 lindssn ⊢ ( ( 𝑉 ∈ LVec ∧ ( 1r ‘ 𝑉 ) ∈ ( Base ‘ 𝑉 ) ∧ ( 1r ‘ 𝑉 ) ≠ ( 0g ‘ 𝑉 ) ) → { ( 1r ‘ 𝑉 ) } ∈ ( LIndS ‘ 𝑉 ) )
29 14 22 27 28 syl3anc ⊢ ( 𝐹 ∈ Field → { ( 1r ‘ 𝑉 ) } ∈ ( LIndS ‘ 𝑉 ) )
30 rspval ⊢ ( RSpan ‘ 𝐹 ) = ( LSpan ‘ ( ringLMod ‘ 𝐹 ) )
31 1 fveq2i ⊢ ( LSpan ‘ 𝑉 ) = ( LSpan ‘ ( ringLMod ‘ 𝐹 ) )
32 30 31 eqtr4i ⊢ ( RSpan ‘ 𝐹 ) = ( LSpan ‘ 𝑉 )
33 32 fveq1i ⊢ ( ( RSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) = ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝐹 ) } )
34 eqid ⊢ ( RSpan ‘ 𝐹 ) = ( RSpan ‘ 𝐹 )
35 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
36 34 4 35 rsp1 ⊢ ( 𝐹 ∈ Ring → ( ( RSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) = ( Base ‘ 𝐹 ) )
37 33 36 eqtr3id ⊢ ( 𝐹 ∈ Ring → ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝐹 ) } ) = ( Base ‘ 𝐹 ) )
38 3 7 37 3syl ⊢ ( 𝐹 ∈ Field → ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝐹 ) } ) = ( Base ‘ 𝐹 ) )
39 11 a1i ⊢ ( 𝐹 ∈ Field → 𝑉 = ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐹 ) ) )
40 eqidd ⊢ ( 𝐹 ∈ Field → ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 ) )
41 39 40 16 sra1r ⊢ ( 𝐹 ∈ Field → ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝑉 ) )
42 41 sneqd ⊢ ( 𝐹 ∈ Field → { ( 1r ‘ 𝐹 ) } = { ( 1r ‘ 𝑉 ) } )
43 42 fveq2d ⊢ ( 𝐹 ∈ Field → ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝐹 ) } ) = ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝑉 ) } ) )
44 39 16 srabase ⊢ ( 𝐹 ∈ Field → ( Base ‘ 𝐹 ) = ( Base ‘ 𝑉 ) )
45 38 43 44 3eqtr3d ⊢ ( 𝐹 ∈ Field → ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝑉 ) } ) = ( Base ‘ 𝑉 ) )
46 eqid ⊢ ( LBasis ‘ 𝑉 ) = ( LBasis ‘ 𝑉 )
47 eqid ⊢ ( LSpan ‘ 𝑉 ) = ( LSpan ‘ 𝑉 )
48 19 46 47 islbs4 ⊢ ( { ( 1r ‘ 𝑉 ) } ∈ ( LBasis ‘ 𝑉 ) ↔ ( { ( 1r ‘ 𝑉 ) } ∈ ( LIndS ‘ 𝑉 ) ∧ ( ( LSpan ‘ 𝑉 ) ‘ { ( 1r ‘ 𝑉 ) } ) = ( Base ‘ 𝑉 ) ) )
49 29 45 48 sylanbrc ⊢ ( 𝐹 ∈ Field → { ( 1r ‘ 𝑉 ) } ∈ ( LBasis ‘ 𝑉 ) )
50 46 dimval ⊢ ( ( 𝑉 ∈ LVec ∧ { ( 1r ‘ 𝑉 ) } ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ { ( 1r ‘ 𝑉 ) } ) )
51 14 49 50 syl2anc ⊢ ( 𝐹 ∈ Field → ( dim ‘ 𝑉 ) = ( ♯ ‘ { ( 1r ‘ 𝑉 ) } ) )
52 fvex ⊢ ( 1r ‘ 𝑉 ) ∈ V
53 hashsng ⊢ ( ( 1r ‘ 𝑉 ) ∈ V → ( ♯ ‘ { ( 1r ‘ 𝑉 ) } ) = 1 )
54 52 53 ax-mp ⊢ ( ♯ ‘ { ( 1r ‘ 𝑉 ) } ) = 1
55 51 54 eqtrdi ⊢ ( 𝐹 ∈ Field → ( dim ‘ 𝑉 ) = 1 )