Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  matunitlindflem2 Structured version   Visualization version   GIF version

Theorem matunitlindflem2 33719
Description: One direction of matunitlindf 33720. (Contributed by Brendan Leahy, 2-Jun-2021.)
Assertion
Ref Expression
matunitlindflem2 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Proof of Theorem matunitlindflem2
Dummy variables 𝑓 𝑖 𝑗 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2760 . . . . . . 7 (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
2 eqid 2760 . . . . . . 7 (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
31, 2matrcl 20420 . . . . . 6 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V))
43simpld 477 . . . . 5 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin)
54ad3antlr 769 . . . 4 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
6 isfld 18958 . . . . . . 7 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
76simplbi 478 . . . . . 6 (𝑅 ∈ Field → 𝑅 ∈ DivRing)
87anim1i 593 . . . . 5 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
94ad2antrl 766 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin)
10 simpr 479 . . . . . . . . . . . . . . 15 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
11 xpfi 8396 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
1211anidms 680 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
13 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
14 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑅) = (Base‘𝑅)
1513, 14frlmfibas 20307 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
1612, 15sylan2 492 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
171, 13matbas 20421 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
1817ancoms 468 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
1916, 18eqtrd 2794 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
2019eleq2d 2825 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
214, 20sylan2 492 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
22 fvex 6362 . . . . . . . . . . . . . . . . . 18 (Base‘𝑅) ∈ V
234, 4, 11syl2anc 696 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 × 𝐼) ∈ Fin)
24 elmapg 8036 . . . . . . . . . . . . . . . . . 18 (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2522, 23, 24sylancr 698 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2625adantl 473 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2721, 26bitr3d 270 . . . . . . . . . . . . . . 15 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2810, 27mpbid 222 . . . . . . . . . . . . . 14 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
2928adantrr 755 . . . . . . . . . . . . 13 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
30 eldifsn 4462 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
3130biimpri 218 . . . . . . . . . . . . . . 15 ((𝐼 ∈ Fin ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
324, 31sylan 489 . . . . . . . . . . . . . 14 ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
3332adantl 473 . . . . . . . . . . . . 13 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ (Fin ∖ {∅}))
34 curf 33700 . . . . . . . . . . . . . 14 ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅}) ∧ (Base‘𝑅) ∈ V) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
3522, 34mp3an3 1562 . . . . . . . . . . . . 13 ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅})) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
3629, 33, 35syl2anc 696 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
379, 36jca 555 . . . . . . . . . . 11 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)))
3837ex 449 . . . . . . . . . 10 (𝑅 ∈ DivRing → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
3938imdistani 728 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
4039anassrs 683 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
41 anass 684 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ↔ (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
4240, 41sylibr 224 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)))
43 drngring 18956 . . . . . . . . . . . . 13 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
44 eqid 2760 . . . . . . . . . . . . . 14 (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼)
45 eqid 2760 . . . . . . . . . . . . . 14 (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
46 eqid 2760 . . . . . . . . . . . . . 14 (Base‘(𝑅 freeLMod 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))
4744, 45, 46uvcff 20332 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
4843, 47sylan 489 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
4948ffvelrnda 6522 . . . . . . . . . . 11 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
5049ad4ant14 1209 . . . . . . . . . 10 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
51 ffn 6206 . . . . . . . . . . . . . . . 16 (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → curry 𝑀 Fn 𝐼)
52 fnima 6171 . . . . . . . . . . . . . . . 16 (curry 𝑀 Fn 𝐼 → (curry 𝑀𝐼) = ran curry 𝑀)
5351, 52syl 17 . . . . . . . . . . . . . . 15 (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → (curry 𝑀𝐼) = ran curry 𝑀)
5453adantl 473 . . . . . . . . . . . . . 14 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (curry 𝑀𝐼) = ran curry 𝑀)
5554fveq2d 6356 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
5655adantr 472 . . . . . . . . . . . 12 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
57 simplll 815 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝑅 ∈ DivRing)
58 simpllr 817 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
5945frlmlmod 20295 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
6043, 59sylan 489 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
6160adantr 472 . . . . . . . . . . . . . . 15 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
62 lindfrn 20362 . . . . . . . . . . . . . . 15 (((𝑅 freeLMod 𝐼) ∈ LMod ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
6361, 62sylan 489 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
6445frlmsca 20299 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
65 drngnzr 19464 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
6665adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing)
6764, 66eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)
6860, 67jca 555 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing))
69 eqid 2760 . . . . . . . . . . . . . . . . . . . . . 22 (Scalar‘(𝑅 freeLMod 𝐼)) = (Scalar‘(𝑅 freeLMod 𝐼))
7046, 69lindff1 20361 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)))
71703expa 1112 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)))
7268, 71sylan 489 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)))
73 fdm 6212 . . . . . . . . . . . . . . . . . . 19 (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → dom curry 𝑀 = 𝐼)
74 f1eq2 6258 . . . . . . . . . . . . . . . . . . . 20 (dom curry 𝑀 = 𝐼 → (curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)) ↔ curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼))))
7574biimpac 504 . . . . . . . . . . . . . . . . . . 19 ((curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)) ∧ dom curry 𝑀 = 𝐼) → curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)))
7672, 73, 75syl2an 495 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)))
7776an32s 881 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)))
78 f1f1orn 6309 . . . . . . . . . . . . . . . . 17 (curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼1-1-onto→ran curry 𝑀)
7977, 78syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼1-1-onto→ran curry 𝑀)
80 f1oeng 8140 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ Fin ∧ curry 𝑀:𝐼1-1-onto→ran curry 𝑀) → 𝐼 ≈ ran curry 𝑀)
8158, 79, 80syl2anc 696 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ≈ ran curry 𝑀)
8281ensymd 8172 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀𝐼)
83 lindsenlbs 33717 . . . . . . . . . . . . . 14 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ran curry 𝑀𝐼) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
8457, 58, 63, 82, 83syl31anc 1480 . . . . . . . . . . . . 13 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
85 eqid 2760 . . . . . . . . . . . . . 14 (LBasis‘(𝑅 freeLMod 𝐼)) = (LBasis‘(𝑅 freeLMod 𝐼))
86 eqid 2760 . . . . . . . . . . . . . 14 (LSpan‘(𝑅 freeLMod 𝐼)) = (LSpan‘(𝑅 freeLMod 𝐼))
8746, 85, 86lbssp 19281 . . . . . . . . . . . . 13 (ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
8884, 87syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
8956, 88eqtrd 2794 . . . . . . . . . . 11 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
9089adantr 472 . . . . . . . . . 10 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
9150, 90eleqtrrd 2842 . . . . . . . . 9 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)))
92 eqid 2760 . . . . . . . . . . . . 13 (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))
93 eqid 2760 . . . . . . . . . . . . 13 (0g‘(Scalar‘(𝑅 freeLMod 𝐼))) = (0g‘(Scalar‘(𝑅 freeLMod 𝐼)))
94 eqid 2760 . . . . . . . . . . . . 13 ( ·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠 ‘(𝑅 freeLMod 𝐼))
9545, 14frlmfibas 20307 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
9695feq3d 6193 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ↔ curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼))))
9796biimpa 502 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
9859adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
99 simplr 809 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → 𝐼 ∈ Fin)
10086, 46, 92, 69, 93, 94, 97, 98, 99elfilspd 20344 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
10145frlmsca 20299 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
102101fveq2d 6356 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘𝑅) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))))
103102oveq1d 6828 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼))
104103adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → ((Base‘𝑅) ↑𝑚 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼))
105 elmapi 8045 . . . . . . . . . . . . . . 15 (𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼) → 𝑛:𝐼⟶(Base‘𝑅))
106 ffn 6206 . . . . . . . . . . . . . . . . . . . 20 (𝑛:𝐼⟶(Base‘𝑅) → 𝑛 Fn 𝐼)
107106adantl 473 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑛 Fn 𝐼)
10851ad2antlr 765 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀 Fn 𝐼)
109 simpllr 817 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝐼 ∈ Fin)
110 inidm 3965 . . . . . . . . . . . . . . . . . . 19 (𝐼𝐼) = 𝐼
111 eqidd 2761 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑛𝑘) = (𝑛𝑘))
112 eqidd 2761 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) = (curry 𝑀𝑘))
113107, 108, 109, 109, 110, 111, 112offval 7069 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘𝐼 ↦ ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘))))
114 simp-4r 827 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → 𝐼 ∈ Fin)
115 ffvelrn 6520 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛:𝐼⟶(Base‘𝑅) ∧ 𝑘𝐼) → (𝑛𝑘) ∈ (Base‘𝑅))
116115adantll 752 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑛𝑘) ∈ (Base‘𝑅))
117 ffvelrn 6520 . . . . . . . . . . . . . . . . . . . . . . 23 ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘𝐼) → (curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼))
118117ad4ant24 1213 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼))
11995ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((Base‘𝑅) ↑𝑚 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
120118, 119eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) ∈ (Base‘(𝑅 freeLMod 𝐼)))
121 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (.r𝑅) = (.r𝑅)
12245, 46, 14, 114, 116, 120, 94, 121frlmvscafval 20311 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘)) = ((𝐼 × {(𝑛𝑘)}) ∘𝑓 (.r𝑅)(curry 𝑀𝑘)))
123 fvex 6362 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘) ∈ V
124 fnconstg 6254 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑘) ∈ V → (𝐼 × {(𝑛𝑘)}) Fn 𝐼)
125123, 124mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝐼 × {(𝑛𝑘)}) Fn 𝐼)
126 elmapfn 8046 . . . . . . . . . . . . . . . . . . . . . . 23 ((curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼) → (curry 𝑀𝑘) Fn 𝐼)
127117, 126syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘𝐼) → (curry 𝑀𝑘) Fn 𝐼)
128127ad4ant24 1213 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) Fn 𝐼)
129123fvconst2 6633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝐼 → ((𝐼 × {(𝑛𝑘)})‘𝑗) = (𝑛𝑘))
130129adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((𝐼 × {(𝑛𝑘)})‘𝑗) = (𝑛𝑘))
131 eqidd 2761 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((curry 𝑀𝑘)‘𝑗) = ((curry 𝑀𝑘)‘𝑗))
132125, 128, 114, 114, 110, 130, 131offval 7069 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝐼 × {(𝑛𝑘)}) ∘𝑓 (.r𝑅)(curry 𝑀𝑘)) = (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))
133122, 132eqtrd 2794 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘)) = (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))
134133mpteq2dva 4896 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘𝐼 ↦ ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘))) = (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))
135113, 134eqtrd 2794 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))
136135oveq2d 6829 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)) = ((𝑅 freeLMod 𝐼) Σg (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
137 eqid 2760 . . . . . . . . . . . . . . . . 17 (0g‘(𝑅 freeLMod 𝐼)) = (0g‘(𝑅 freeLMod 𝐼))
138 simplll 815 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑅 ∈ Ring)
139 simp-5l 829 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → 𝑅 ∈ Ring)
140115ad4ant23 1211 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → (𝑛𝑘) ∈ (Base‘𝑅))
141 simplr 809 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
142 elmapi 8045 . . . . . . . . . . . . . . . . . . . . . . 23 ((curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼) → (curry 𝑀𝑘):𝐼⟶(Base‘𝑅))
143117, 142syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘𝐼) → (curry 𝑀𝑘):𝐼⟶(Base‘𝑅))
144143ffvelrnda 6522 . . . . . . . . . . . . . . . . . . . . 21 (((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((curry 𝑀𝑘)‘𝑗) ∈ (Base‘𝑅))
145141, 144sylanl1 685 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((curry 𝑀𝑘)‘𝑗) ∈ (Base‘𝑅))
14614, 121ringcl 18761 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Ring ∧ (𝑛𝑘) ∈ (Base‘𝑅) ∧ ((curry 𝑀𝑘)‘𝑗) ∈ (Base‘𝑅)) → ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)) ∈ (Base‘𝑅))
147139, 140, 145, 146syl3anc 1477 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)) ∈ (Base‘𝑅))
148 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) = (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))
149147, 148fmptd 6548 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅))
150 elmapg 8036 . . . . . . . . . . . . . . . . . . . . . 22 (((Base‘𝑅) ∈ V ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
15122, 150mpan 708 . . . . . . . . . . . . . . . . . . . . 21 (𝐼 ∈ Fin → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
152151adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
15395eleq2d 2825 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
154152, 153bitr3d 270 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
155154ad3antrrr 768 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
156149, 155mpbid 222 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼)))
157 mptexg 6648 . . . . . . . . . . . . . . . . . . . . 21 (𝐼 ∈ Fin → (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ V)
158157ralrimivw 3105 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ Fin → ∀𝑘𝐼 (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ V)
159 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) = (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))
160159fnmpt 6181 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝐼 (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ V → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) Fn 𝐼)
161158, 160syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ Fin → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) Fn 𝐼)
162 id 22 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ Fin → 𝐼 ∈ Fin)
163 fvexd 6364 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ Fin → (0g‘(𝑅 freeLMod 𝐼)) ∈ V)
164161, 162, 163fndmfifsupp 8453 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ Fin → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
165164ad3antlr 769 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
16645, 46, 137, 109, 109, 138, 156, 165frlmgsum 20313 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
167136, 166eqtr2d 2795 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
168105, 167sylan2 492 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
169168eqeq2d 2770 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
170104, 169rexeqbidva 3294 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
171100, 170bitr4d 271 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))))
17243, 171sylanl1 685 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))))
173172ad2antrr 764 . . . . . . . . 9 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))))
17491, 173mpbid 222 . . . . . . . 8 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
175174ralrimiva 3104 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
17642, 175sylan 489 . . . . . 6 ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
17710, 21mpbird 247 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
178 elmapfn 8046 . . . . . . . . 9 (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) → 𝑀 Fn (𝐼 × 𝐼))
179177, 178syl 17 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 Fn (𝐼 × 𝐼))
1804adantl 473 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝐼 ∈ Fin)
181 an32 874 . . . . . . . . . . . . . . . . . . 19 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝑘𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼) ∧ 𝑗𝐼))
182 df-3an 1074 . . . . . . . . . . . . . . . . . . 19 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼𝑗𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼) ∧ 𝑗𝐼))
183181, 182bitr4i 267 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝑘𝐼) ↔ (𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼𝑗𝐼))
184 curfv 33702 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼𝑗𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀𝑘)‘𝑗) = (𝑘𝑀𝑗))
185183, 184sylanb 490 . . . . . . . . . . . . . . . . 17 ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝑘𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀𝑘)‘𝑗) = (𝑘𝑀𝑗))
186185an32s 881 . . . . . . . . . . . . . . . 16 ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘𝐼) → ((curry 𝑀𝑘)‘𝑗) = (𝑘𝑀𝑗))
187186oveq2d 6829 . . . . . . . . . . . . . . 15 ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘𝐼) → ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)) = ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))
188187mpteq2dva 4896 . . . . . . . . . . . . . 14 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝐼 ∈ Fin) → (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) = (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))
189188an32s 881 . . . . . . . . . . . . 13 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗𝐼) → (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) = (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))
190189oveq2d 6829 . . . . . . . . . . . 12 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗𝐼) → (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
191190mpteq2dva 4896 . . . . . . . . . . 11 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
192191eqeq2d 2770 . . . . . . . . . 10 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
193192rexbidv 3190 . . . . . . . . 9 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
194193ralbidv 3124 . . . . . . . 8 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
195179, 180, 194syl2anc 696 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
196195ad2antrr 764 . . . . . 6 ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → (∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
197176, 196mpbid 222 . . . . 5 ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
1988, 197sylanl1 685 . . . 4 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
199 fveq1 6351 . . . . . . . . . . 11 (𝑛 = (𝑓𝑖) → (𝑛𝑘) = ((𝑓𝑖)‘𝑘))
200 vex 3343 . . . . . . . . . . . 12 𝑖 ∈ V
201 vex 3343 . . . . . . . . . . . 12 𝑘 ∈ V
202 uncov 33703 . . . . . . . . . . . 12 ((𝑖 ∈ V ∧ 𝑘 ∈ V) → (𝑖uncurry 𝑓𝑘) = ((𝑓𝑖)‘𝑘))
203200, 201, 202mp2an 710 . . . . . . . . . . 11 (𝑖uncurry 𝑓𝑘) = ((𝑓𝑖)‘𝑘)
204199, 203syl6eqr 2812 . . . . . . . . . 10 (𝑛 = (𝑓𝑖) → (𝑛𝑘) = (𝑖uncurry 𝑓𝑘))
205204oveq1d 6828 . . . . . . . . 9 (𝑛 = (𝑓𝑖) → ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)) = ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))
206205mpteq2dv 4897 . . . . . . . 8 (𝑛 = (𝑓𝑖) → (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))) = (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))
207206oveq2d 6829 . . . . . . 7 (𝑛 = (𝑓𝑖) → (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
208207mpteq2dv 4897 . . . . . 6 (𝑛 = (𝑓𝑖) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
209208eqeq2d 2770 . . . . 5 (𝑛 = (𝑓𝑖) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
210209ac6sfi 8369 . . . 4 ((𝐼 ∈ Fin ∧ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
2115, 198, 210syl2anc 696 . . 3 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
212 uncf 33701 . . . . . . 7 (𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅))
21313, 14frlmfibas 20307 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
21412, 213sylan2 492 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
2151, 13matbas 20421 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
216215ancoms 468 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
217214, 216eqtrd 2794 . . . . . . . . . . . . . 14 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
2184, 217sylan2 492 . . . . . . . . . . . . 13 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
219218eleq2d 2825 . . . . . . . . . . . 12 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅))))
220 elmapg 8036 . . . . . . . . . . . . . 14 (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
22122, 23, 220sylancr 698 . . . . . . . . . . . . 13 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
222221adantl 473 . . . . . . . . . . . 12 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
223219, 222bitr3d 270 . . . . . . . . . . 11 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
224223biimpar 503 . . . . . . . . . 10 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
225224adantr 472 . . . . . . . . 9 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
226 nfv 1992 . . . . . . . . . . . . . 14 𝑗(((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼)
227 nfmpt1 4899 . . . . . . . . . . . . . . 15 𝑗(𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
228227nfeq2 2918 . . . . . . . . . . . . . 14 𝑗((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
229 fveq1 6351 . . . . . . . . . . . . . . . . 17 (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗))
2307, 43syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Field → 𝑅 ∈ Ring)
231230, 4anim12i 591 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
232231adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
233 equcom 2100 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑗𝑗 = 𝑖)
234 ifbi 4251 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 = 𝑗𝑗 = 𝑖) → if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅)))
235233, 234ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅))
236 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (1r𝑅) = (1r𝑅)
237 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (0g𝑅) = (0g𝑅)
238 simpllr 817 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝐼 ∈ Fin)
239 simplll 815 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑅 ∈ Ring)
240 simplr 809 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑖𝐼)
241 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑗𝐼)
242 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (1r‘(𝐼 Mat 𝑅)) = (1r‘(𝐼 Mat 𝑅))
2431, 236, 237, 238, 239, 240, 241, 242mat1ov 20456 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)))
244 df-3an 1074 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖𝐼) ↔ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼))
24544, 236, 237uvcvval 20327 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅)))
246244, 245sylanbr 491 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅)))
247235, 243, 2463eqtr4a 2820 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
248232, 247sylanl1 685 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
249 ovex 6841 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))) ∈ V
250 eqid 2760 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
251250fvmpt2 6453 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝐼 ∧ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))) ∈ V) → ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
252249, 251mpan2 709 . . . . . . . . . . . . . . . . . . . 20 (𝑗𝐼 → ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
253252adantl 473 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
254 eqid 2760 . . . . . . . . . . . . . . . . . . . 20 (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)
255 simp-4l 825 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑅 ∈ Field)
2564ad4antlr 773 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝐼 ∈ Fin)
257221biimpar 503 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
258257ad5ant23 1222 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
259 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
260259, 218eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
261260ad3antrrr 768 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
262 simplr 809 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑖𝐼)
263 simpr 479 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑗𝐼)
264254, 14, 121, 255, 256, 256, 256, 258, 261, 262, 263mamufv 20395 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
2651, 254matmulr 20446 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
266265ancoms 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
267266oveqd 6830 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
268267oveqd 6830 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
2694, 268sylan2 492 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
270269ad3antrrr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
271253, 264, 2703eqtr2rd 2801 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) = ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗))
272248, 271eqeq12d 2775 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → ((𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) ↔ (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗)))
273229, 272syl5ibr 236 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
274273ex 449 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) → (𝑗𝐼 → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
275274com23 86 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (𝑗𝐼 → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
276226, 228, 275ralrimd 3097 . . . . . . . . . . . . 13 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → ∀𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
277276ralimdva 3100 . . . . . . . . . . . 12 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → ∀𝑖𝐼𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
2781, 2, 242mat1bas 20457 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ (Base‘(𝐼 Mat 𝑅)))
27913, 14frlmfibas 20307 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ Ring ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
28012, 279sylan2 492 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
2811, 13matbas 20421 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
282281ancoms 468 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
283280, 282eqtrd 2794 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
284278, 283eleqtrrd 2842 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
285 elmapfn 8046 . . . . . . . . . . . . . . . 16 ((1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
286284, 285syl 17 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
287230, 4, 286syl2an 495 . . . . . . . . . . . . . 14 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
288287adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
2891matring 20451 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼 Mat 𝑅) ∈ Ring)
2904, 230, 289syl2anr 496 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝐼 Mat 𝑅) ∈ Ring)
291290adantr 472 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝐼 Mat 𝑅) ∈ Ring)
292 simplr 809 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
293 eqid 2760 . . . . . . . . . . . . . . . . 17 (.r‘(𝐼 Mat 𝑅)) = (.r‘(𝐼 Mat 𝑅))
2942, 293ringcl 18761 . . . . . . . . . . . . . . . 16 (((𝐼 Mat 𝑅) ∈ Ring ∧ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
295291, 224, 292, 294syl3anc 1477 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
296218adantr 472 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
297295, 296eleqtrrd 2842 . . . . . . . . . . . . . 14 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
298 elmapfn 8046 . . . . . . . . . . . . . 14 ((uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
299297, 298syl 17 . . . . . . . . . . . . 13 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
300 eqfnov2 6932 . . . . . . . . . . . . 13 (((1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖𝐼𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
301288, 299, 300syl2anc 696 . . . . . . . . . . . 12 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖𝐼𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
302277, 301sylibrd 249 . . . . . . . . . . 11 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)))
303302imp 444 . . . . . . . . . 10 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
304303eqcomd 2766 . . . . . . . . 9 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
305 oveq1 6820 . . . . . . . . . . 11 (𝑛 = uncurry 𝑓 → (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
306305eqeq1d 2762 . . . . . . . . . 10 (𝑛 = uncurry 𝑓 → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) ↔ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
307306rspcev 3449 . . . . . . . . 9 ((uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
308225, 304, 307syl2anc 696 . . . . . . . 8 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
309308expl 649 . . . . . . 7 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
310212, 309sylani 689 . . . . . 6 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
311310exlimdv 2010 . . . . 5 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
312311imp 444 . . . 4 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
313312adantlr 753 . . 3 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
314211, 313syldan 488 . 2 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
3156simprbi 483 . . . 4 (𝑅 ∈ Field → 𝑅 ∈ CRing)
316 eqid 2760 . . . . . . . . . 10 (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
317316, 1, 2, 14mdetcl 20604 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
318316, 1, 2, 14mdetcl 20604 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅))
319 eqid 2760 . . . . . . . . . 10 (∥r𝑅) = (∥r𝑅)
32014, 319, 121dvdsrmul 18848 . . . . . . . . 9 ((((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅)) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
321317, 318, 320syl2an 495 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
322321anandis 908 . . . . . . 7 ((𝑅 ∈ CRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
323322anassrs 683 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
324323adantrr 755 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
325 fveq2 6352 . . . . . . . . 9 ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))))
3261, 2, 316, 121, 293mdetmul 20631 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
3273263expa 1112 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
328327an32s 881 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
329316, 1, 242, 236mdet1 20609 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝐼 ∈ Fin) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r𝑅))
3304, 329sylan2 492 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r𝑅))
331330adantr 472 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r𝑅))
332328, 331eqeq12d 2775 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) ↔ (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r𝑅)))
333325, 332syl5ib 234 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r𝑅)))
334333impr 650 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r𝑅))
335334breq2d 4816 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(1r𝑅)))
336 eqid 2760 . . . . . . . 8 (Unit‘𝑅) = (Unit‘𝑅)
337336, 236, 319crngunit 18862 . . . . . . 7 (𝑅 ∈ CRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(1r𝑅)))
338337ad2antrr 764 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(1r𝑅)))
339335, 338bitr4d 271 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
340324, 339mpbid 222 . . . 4 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
341315, 340sylanl1 685 . . 3 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
342341ad4ant14 1209 . 2 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
343314, 342rexlimddv 3173 1 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  cdif 3712  c0 4058  ifcif 4230  {csn 4321  cotp 4329   class class class wbr 4804  cmpt 4881   × cxp 5264  dom cdm 5266  ran crn 5267  cima 5269   Fn wfn 6044  wf 6045  1-1wf1 6046  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6813  𝑓 cof 7060  curry ccur 7560  uncurry cunc 7561  𝑚 cmap 8023  cen 8118  Fincfn 8121   finSupp cfsupp 8440  Basecbs 16059  .rcmulr 16144  Scalarcsca 16146   ·𝑠 cvsca 16147  0gc0g 16302   Σg cgsu 16303  1rcur 18701  Ringcrg 18747  CRingccrg 18748  rcdsr 18838  Unitcui 18839  DivRingcdr 18949  Fieldcfield 18950  LModclmod 19065  LSpanclspn 19173  LBasisclbs 19276  NzRingcnzr 19459   freeLMod cfrlm 20292   unitVec cuvc 20323   LIndF clindf 20345  LIndSclinds 20346   maMul cmmul 20391   Mat cmat 20415   maDet cmdat 20592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-xor 1614  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-ot 4330  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-tpos 7521  df-cur 7562  df-unc 7563  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-sup 8513  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-xnn0 11556  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-hash 13312  df-word 13485  df-lsw 13486  df-concat 13487  df-s1 13488  df-substr 13489  df-splice 13490  df-reverse 13491  df-s2 13793  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-0g 16304  df-gsum 16305  df-prds 16310  df-pws 16312  df-mre 16448  df-mrc 16449  df-mri 16450  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-ghm 17859  df-gim 17902  df-cntz 17950  df-oppg 17976  df-symg 17998  df-pmtr 18062  df-psgn 18111  df-evpm 18112  df-cmn 18395  df-abl 18396  df-mgp 18690  df-ur 18702  df-srg 18706  df-ring 18749  df-cring 18750  df-oppr 18823  df-dvdsr 18841  df-unit 18842  df-invr 18872  df-dvr 18883  df-rnghom 18917  df-drng 18951  df-field 18952  df-subrg 18980  df-lmod 19067  df-lss 19135  df-lsp 19174  df-lmhm 19224  df-lbs 19277  df-lvec 19305  df-sra 19374  df-rgmod 19375  df-nzr 19460  df-cnfld 19949  df-zring 20021  df-zrh 20054  df-dsmm 20278  df-frlm 20293  df-uvc 20324  df-lindf 20347  df-linds 20348  df-mamu 20392  df-mat 20416  df-mdet 20593
This theorem is referenced by:  matunitlindf  33720
  Copyright terms: Public domain W3C validator