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 34775
Description: One direction of matunitlindf 34776. (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 2826 . . . . . . 7 (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
2 eqid 2826 . . . . . . 7 (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
31, 2matrcl 20956 . . . . . 6 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V))
43simpld 495 . . . . 5 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin)
54ad3antlr 727 . . . 4 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
6 isfld 19447 . . . . . . 7 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
76simplbi 498 . . . . . 6 (𝑅 ∈ Field → 𝑅 ∈ DivRing)
87anim1i 614 . . . . 5 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
94ad2antrl 724 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin)
10 simpr 485 . . . . . . . . . . . . . . 15 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
11 xpfi 8783 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
1211anidms 567 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
13 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
14 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑅) = (Base‘𝑅)
1513, 14frlmfibas 20841 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
1612, 15sylan2 592 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
171, 13matbas 20957 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
1817ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
1916, 18eqtrd 2861 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
2019eleq2d 2903 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
214, 20sylan2 592 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
22 fvex 6682 . . . . . . . . . . . . . . . . . 18 (Base‘𝑅) ∈ V
234, 4, 11syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 × 𝐼) ∈ Fin)
24 elmapg 8414 . . . . . . . . . . . . . . . . . 18 (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2522, 23, 24sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2625adantl 482 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2721, 26bitr3d 282 . . . . . . . . . . . . . . 15 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
2810, 27mpbid 233 . . . . . . . . . . . . . 14 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
2928adantrr 713 . . . . . . . . . . . . 13 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
30 eldifsn 4718 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
3130biimpri 229 . . . . . . . . . . . . . . 15 ((𝐼 ∈ Fin ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
324, 31sylan 580 . . . . . . . . . . . . . 14 ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
3332adantl 482 . . . . . . . . . . . . 13 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ (Fin ∖ {∅}))
34 curf 34756 . . . . . . . . . . . . . 14 ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅}) ∧ (Base‘𝑅) ∈ V) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
3522, 34mp3an3 1443 . . . . . . . . . . . . 13 ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅})) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
3629, 33, 35syl2anc 584 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
379, 36jca 512 . . . . . . . . . . 11 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)))
3837ex 413 . . . . . . . . . 10 (𝑅 ∈ DivRing → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
3938imdistani 569 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
4039anassrs 468 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
41 anass 469 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ↔ (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
4240, 41sylibr 235 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)))
43 drngring 19445 . . . . . . . . . . . . 13 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
44 eqid 2826 . . . . . . . . . . . . . 14 (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼)
45 eqid 2826 . . . . . . . . . . . . . 14 (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
46 eqid 2826 . . . . . . . . . . . . . 14 (Base‘(𝑅 freeLMod 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))
4744, 45, 46uvcff 20870 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
4843, 47sylan 580 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
4948ffvelrnda 6849 . . . . . . . . . . 11 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
5049ad4ant14 748 . . . . . . . . . 10 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
51 ffn 6513 . . . . . . . . . . . . . . . 16 (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → curry 𝑀 Fn 𝐼)
52 fnima 6477 . . . . . . . . . . . . . . . 16 (curry 𝑀 Fn 𝐼 → (curry 𝑀𝐼) = ran curry 𝑀)
5351, 52syl 17 . . . . . . . . . . . . . . 15 (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → (curry 𝑀𝐼) = ran curry 𝑀)
5453adantl 482 . . . . . . . . . . . . . 14 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (curry 𝑀𝐼) = ran curry 𝑀)
5554fveq2d 6673 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
5655adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
57 simplll 771 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝑅 ∈ DivRing)
58 simpllr 772 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
5945frlmlmod 20828 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
6043, 59sylan 580 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
6160adantr 481 . . . . . . . . . . . . . . 15 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
62 lindfrn 20900 . . . . . . . . . . . . . . 15 (((𝑅 freeLMod 𝐼) ∈ LMod ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
6361, 62sylan 580 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
6445frlmsca 20832 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
65 drngnzr 19970 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
6665adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing)
6764, 66eqeltrrd 2919 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)
6860, 67jca 512 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing))
69 eqid 2826 . . . . . . . . . . . . . . . . . . . . . 22 (Scalar‘(𝑅 freeLMod 𝐼)) = (Scalar‘(𝑅 freeLMod 𝐼))
7046, 69lindff1 20899 . . . . . . . . . . . . . . . . . . . . 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 580 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)))
73 fdm 6521 . . . . . . . . . . . . . . . . . . 19 (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → dom curry 𝑀 = 𝐼)
74 f1eq2 6570 . . . . . . . . . . . . . . . . . . . 20 (dom curry 𝑀 = 𝐼 → (curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)) ↔ curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼))))
7574biimpac 479 . . . . . . . . . . . . . . . . . . 19 ((curry 𝑀:dom curry 𝑀1-1→(Base‘(𝑅 freeLMod 𝐼)) ∧ dom curry 𝑀 = 𝐼) → curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)))
7672, 73, 75syl2an 595 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)))
7776an32s 648 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)))
78 f1f1orn 6625 . . . . . . . . . . . . . . . . 17 (curry 𝑀:𝐼1-1→(Base‘(𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼1-1-onto→ran curry 𝑀)
7977, 78syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼1-1-onto→ran curry 𝑀)
80 f1oeng 8522 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ Fin ∧ curry 𝑀:𝐼1-1-onto→ran curry 𝑀) → 𝐼 ≈ ran curry 𝑀)
8158, 79, 80syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ≈ ran curry 𝑀)
8281ensymd 8554 . . . . . . . . . . . . . 14 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀𝐼)
83 lindsenlbs 34773 . . . . . . . . . . . . . 14 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ran curry 𝑀𝐼) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
8457, 58, 63, 82, 83syl31anc 1367 . . . . . . . . . . . . 13 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
85 eqid 2826 . . . . . . . . . . . . . 14 (LBasis‘(𝑅 freeLMod 𝐼)) = (LBasis‘(𝑅 freeLMod 𝐼))
86 eqid 2826 . . . . . . . . . . . . . 14 (LSpan‘(𝑅 freeLMod 𝐼)) = (LSpan‘(𝑅 freeLMod 𝐼))
8746, 85, 86lbssp 19787 . . . . . . . . . . . . 13 (ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
8884, 87syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
8956, 88eqtrd 2861 . . . . . . . . . . 11 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
9089adantr 481 . . . . . . . . . 10 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
9150, 90eleqtrrd 2921 . . . . . . . . 9 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)))
92 eqid 2826 . . . . . . . . . . . . 13 (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))
93 eqid 2826 . . . . . . . . . . . . 13 (0g‘(Scalar‘(𝑅 freeLMod 𝐼))) = (0g‘(Scalar‘(𝑅 freeLMod 𝐼)))
94 eqid 2826 . . . . . . . . . . . . 13 ( ·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠 ‘(𝑅 freeLMod 𝐼))
9545, 14frlmfibas 20841 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
9695feq3d 6500 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ↔ curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼))))
9796biimpa 477 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
9859adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
99 simplr 765 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → 𝐼 ∈ Fin)
10086, 46, 92, 69, 93, 94, 97, 98, 99elfilspd 20882 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
10145frlmsca 20832 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
102101fveq2d 6673 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘𝑅) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))))
103102oveq1d 7165 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼))
104103adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → ((Base‘𝑅) ↑m 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼))
105 elmapi 8423 . . . . . . . . . . . . . . 15 (𝑛 ∈ ((Base‘𝑅) ↑m 𝐼) → 𝑛:𝐼⟶(Base‘𝑅))
106 ffn 6513 . . . . . . . . . . . . . . . . . . . 20 (𝑛:𝐼⟶(Base‘𝑅) → 𝑛 Fn 𝐼)
107106adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑛 Fn 𝐼)
10851ad2antlr 723 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀 Fn 𝐼)
109 simpllr 772 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝐼 ∈ Fin)
110 inidm 4199 . . . . . . . . . . . . . . . . . . 19 (𝐼𝐼) = 𝐼
111 eqidd 2827 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑛𝑘) = (𝑛𝑘))
112 eqidd 2827 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) = (curry 𝑀𝑘))
113107, 108, 109, 109, 110, 111, 112offval 7410 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘𝐼 ↦ ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘))))
114 simp-4r 780 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → 𝐼 ∈ Fin)
115 ffvelrn 6847 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛:𝐼⟶(Base‘𝑅) ∧ 𝑘𝐼) → (𝑛𝑘) ∈ (Base‘𝑅))
116115adantll 710 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑛𝑘) ∈ (Base‘𝑅))
117 ffvelrn 6847 . . . . . . . . . . . . . . . . . . . . . . 23 ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘𝐼) → (curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
118117ad4ant24 750 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
11995ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
120118, 119eleqtrd 2920 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) ∈ (Base‘(𝑅 freeLMod 𝐼)))
121 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (.r𝑅) = (.r𝑅)
12245, 46, 14, 114, 116, 120, 94, 121frlmvscafval 20845 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘)) = ((𝐼 × {(𝑛𝑘)}) ∘f (.r𝑅)(curry 𝑀𝑘)))
123 fvex 6682 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛𝑘) ∈ V
124 fnconstg 6566 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛𝑘) ∈ V → (𝐼 × {(𝑛𝑘)}) Fn 𝐼)
125123, 124mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝐼 × {(𝑛𝑘)}) Fn 𝐼)
126 elmapfn 8424 . . . . . . . . . . . . . . . . . . . . . . 23 ((curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀𝑘) Fn 𝐼)
127117, 126syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘𝐼) → (curry 𝑀𝑘) Fn 𝐼)
128127ad4ant24 750 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (curry 𝑀𝑘) Fn 𝐼)
129123fvconst2 6964 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝐼 → ((𝐼 × {(𝑛𝑘)})‘𝑗) = (𝑛𝑘))
130129adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((𝐼 × {(𝑛𝑘)})‘𝑗) = (𝑛𝑘))
131 eqidd 2827 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((curry 𝑀𝑘)‘𝑗) = ((curry 𝑀𝑘)‘𝑗))
132125, 128, 114, 114, 110, 130, 131offval 7410 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝐼 × {(𝑛𝑘)}) ∘f (.r𝑅)(curry 𝑀𝑘)) = (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))
133122, 132eqtrd 2861 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘)) = (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))
134133mpteq2dva 5158 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘𝐼 ↦ ((𝑛𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀𝑘))) = (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))
135113, 134eqtrd 2861 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))
136135oveq2d 7166 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)) = ((𝑅 freeLMod 𝐼) Σg (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
137 eqid 2826 . . . . . . . . . . . . . . . . 17 (0g‘(𝑅 freeLMod 𝐼)) = (0g‘(𝑅 freeLMod 𝐼))
138 simplll 771 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑅 ∈ Ring)
139 simp-5l 781 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → 𝑅 ∈ Ring)
140115ad4ant23 749 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → (𝑛𝑘) ∈ (Base‘𝑅))
141 simplr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
142 elmapi 8423 . . . . . . . . . . . . . . . . . . . . . . 23 ((curry 𝑀𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀𝑘):𝐼⟶(Base‘𝑅))
143117, 142syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘𝐼) → (curry 𝑀𝑘):𝐼⟶(Base‘𝑅))
144143ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . 21 (((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((curry 𝑀𝑘)‘𝑗) ∈ (Base‘𝑅))
145141, 144sylanl1 676 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((curry 𝑀𝑘)‘𝑗) ∈ (Base‘𝑅))
14614, 121ringcl 19247 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Ring ∧ (𝑛𝑘) ∈ (Base‘𝑅) ∧ ((curry 𝑀𝑘)‘𝑗) ∈ (Base‘𝑅)) → ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)) ∈ (Base‘𝑅))
147139, 140, 145, 146syl3anc 1365 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) ∧ 𝑗𝐼) → ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)) ∈ (Base‘𝑅))
148147fmpttd 6877 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅))
149 elmapg 8414 . . . . . . . . . . . . . . . . . . . . . 22 (((Base‘𝑅) ∈ V ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
15022, 149mpan 686 . . . . . . . . . . . . . . . . . . . . 21 (𝐼 ∈ Fin → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
151150adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
15295eleq2d 2903 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
153151, 152bitr3d 282 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
154153ad3antrrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → ((𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
155148, 154mpbid 233 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘𝐼) → (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼)))
156 mptexg 6981 . . . . . . . . . . . . . . . . . . . . 21 (𝐼 ∈ Fin → (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ V)
157156ralrimivw 3188 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ Fin → ∀𝑘𝐼 (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ V)
158 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) = (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))
159158fnmpt 6487 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝐼 (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) ∈ V → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) Fn 𝐼)
160157, 159syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ Fin → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) Fn 𝐼)
161 id 22 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ Fin → 𝐼 ∈ Fin)
162 fvexd 6684 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ Fin → (0g‘(𝑅 freeLMod 𝐼)) ∈ V)
163160, 161, 162fndmfifsupp 8840 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ Fin → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
164163ad3antlr 727 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
16545, 46, 137, 109, 109, 138, 155, 164frlmgsum 20851 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑘𝐼 ↦ (𝑗𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
166136, 165eqtr2d 2862 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
167105, 166sylan2 592 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
168167eqeq2d 2837 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
169104, 168rexeqbidva 3432 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
170100, 169bitr4d 283 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))))
17143, 170sylanl1 676 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))))
172171ad2antrr 722 . . . . . . . . 9 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))))))
17391, 172mpbid 233 . . . . . . . 8 (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖𝐼) → ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
174173ralrimiva 3187 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
17542, 174sylan 580 . . . . . 6 ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))))
17610, 21mpbird 258 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
177 elmapfn 8424 . . . . . . . . 9 (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → 𝑀 Fn (𝐼 × 𝐼))
178176, 177syl 17 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 Fn (𝐼 × 𝐼))
1794adantl 482 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝐼 ∈ Fin)
180 an32 642 . . . . . . . . . . . . . . . . . . 19 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝑘𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼) ∧ 𝑗𝐼))
181 df-3an 1083 . . . . . . . . . . . . . . . . . . 19 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼𝑗𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼) ∧ 𝑗𝐼))
182180, 181bitr4i 279 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝑘𝐼) ↔ (𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼𝑗𝐼))
183 curfv 34758 . . . . . . . . . . . . . . . . . 18 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘𝐼𝑗𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀𝑘)‘𝑗) = (𝑘𝑀𝑗))
184182, 183sylanb 581 . . . . . . . . . . . . . . . . 17 ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝑘𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀𝑘)‘𝑗) = (𝑘𝑀𝑗))
185184an32s 648 . . . . . . . . . . . . . . . 16 ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘𝐼) → ((curry 𝑀𝑘)‘𝑗) = (𝑘𝑀𝑗))
186185oveq2d 7166 . . . . . . . . . . . . . . 15 ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘𝐼) → ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)) = ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))
187186mpteq2dva 5158 . . . . . . . . . . . . . 14 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗𝐼) ∧ 𝐼 ∈ Fin) → (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) = (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))
188187an32s 648 . . . . . . . . . . . . 13 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗𝐼) → (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))) = (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))
189188oveq2d 7166 . . . . . . . . . . . 12 (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗𝐼) → (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗)))) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
190189mpteq2dva 5158 . . . . . . . . . . 11 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
191190eqeq2d 2837 . . . . . . . . . 10 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
192191rexbidv 3302 . . . . . . . . 9 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
193192ralbidv 3202 . . . . . . . 8 ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
194178, 179, 193syl2anc 584 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
195194ad2antrr 722 . . . . . 6 ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → (∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)((curry 𝑀𝑘)‘𝑗))))) ↔ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
196175, 195mpbid 233 . . . . 5 ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
1978, 196sylanl1 676 . . . 4 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
198 fveq1 6668 . . . . . . . . . . 11 (𝑛 = (𝑓𝑖) → (𝑛𝑘) = ((𝑓𝑖)‘𝑘))
199 uncov 34759 . . . . . . . . . . . 12 ((𝑖 ∈ V ∧ 𝑘 ∈ V) → (𝑖uncurry 𝑓𝑘) = ((𝑓𝑖)‘𝑘))
200199el2v 3507 . . . . . . . . . . 11 (𝑖uncurry 𝑓𝑘) = ((𝑓𝑖)‘𝑘)
201198, 200syl6eqr 2879 . . . . . . . . . 10 (𝑛 = (𝑓𝑖) → (𝑛𝑘) = (𝑖uncurry 𝑓𝑘))
202201oveq1d 7165 . . . . . . . . 9 (𝑛 = (𝑓𝑖) → ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)) = ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))
203202mpteq2dv 5159 . . . . . . . 8 (𝑛 = (𝑓𝑖) → (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))) = (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))
204203oveq2d 7166 . . . . . . 7 (𝑛 = (𝑓𝑖) → (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
205204mpteq2dv 5159 . . . . . 6 (𝑛 = (𝑓𝑖) → (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))))
206205eqeq2d 2837 . . . . 5 (𝑛 = (𝑓𝑖) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
207206ac6sfi 8756 . . . 4 ((𝐼 ∈ Fin ∧ ∀𝑖𝐼𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑛𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
2085, 197, 207syl2anc 584 . . 3 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))))
209 uncf 34757 . . . . . . 7 (𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) → uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅))
21013, 14frlmfibas 20841 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
21112, 210sylan2 592 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
2121, 13matbas 20957 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
213212ancoms 459 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
214211, 213eqtrd 2861 . . . . . . . . . . . . . 14 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
2154, 214sylan2 592 . . . . . . . . . . . . 13 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
216215eleq2d 2903 . . . . . . . . . . . 12 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅))))
217 elmapg 8414 . . . . . . . . . . . . . 14 (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
21822, 23, 217sylancr 587 . . . . . . . . . . . . 13 (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
219218adantl 482 . . . . . . . . . . . 12 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
220216, 219bitr3d 282 . . . . . . . . . . 11 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
221220biimpar 478 . . . . . . . . . 10 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
222221adantr 481 . . . . . . . . 9 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
223 nfv 1908 . . . . . . . . . . . . . 14 𝑗(((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼)
224 nfmpt1 5161 . . . . . . . . . . . . . . 15 𝑗(𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
225224nfeq2 3000 . . . . . . . . . . . . . 14 𝑗((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
226 fveq1 6668 . . . . . . . . . . . . . . . . 17 (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗))
2277, 43syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Field → 𝑅 ∈ Ring)
228227, 4anim12i 612 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
229228adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
230 equcom 2018 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑗𝑗 = 𝑖)
231 ifbi 4491 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 = 𝑗𝑗 = 𝑖) → if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅)))
232230, 231ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅))
233 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (1r𝑅) = (1r𝑅)
234 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (0g𝑅) = (0g𝑅)
235 simpllr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝐼 ∈ Fin)
236 simplll 771 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑅 ∈ Ring)
237 simplr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑖𝐼)
238 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑗𝐼)
239 eqid 2826 . . . . . . . . . . . . . . . . . . . . 21 (1r‘(𝐼 Mat 𝑅)) = (1r‘(𝐼 Mat 𝑅))
2401, 233, 234, 235, 236, 237, 238, 239mat1ov 20992 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)))
241 df-3an 1083 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖𝐼) ↔ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼))
24244, 233, 234uvcvval 20865 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅)))
243241, 242sylanbr 582 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r𝑅), (0g𝑅)))
244232, 240, 2433eqtr4a 2887 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
245229, 244sylanl1 676 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
246 ovex 7183 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))) ∈ V
247 eqid 2826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
248247fvmpt2 6777 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝐼 ∧ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))) ∈ V) → ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
249246, 248mpan2 687 . . . . . . . . . . . . . . . . . . . 20 (𝑗𝐼 → ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
250249adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
251 eqid 2826 . . . . . . . . . . . . . . . . . . . 20 (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)
252 simp-4l 779 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑅 ∈ Field)
2534ad4antlr 729 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝐼 ∈ Fin)
254218biimpar 478 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
255254ad5ant23 756 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
256 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
257256, 215eleqtrrd 2921 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
258257ad3antrrr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
259 simplr 765 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑖𝐼)
260 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → 𝑗𝐼)
261251, 14, 121, 252, 253, 253, 253, 255, 258, 259, 260mamufv 20933 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))
2621, 251matmulr 20982 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
263262ancoms 459 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
264263oveqd 7167 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
265264oveqd 7167 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
2664, 265sylan2 592 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
267266ad3antrrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
268250, 261, 2673eqtr2rd 2868 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) = ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗))
269245, 268eqeq12d 2842 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → ((𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) ↔ (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))‘𝑗)))
270226, 269syl5ibr 247 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) ∧ 𝑗𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
271270ex 413 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) → (𝑗𝐼 → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
272271com23 86 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (𝑗𝐼 → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
273223, 225, 272ralrimd 3223 . . . . . . . . . . . . 13 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → ∀𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
274273ralimdva 3182 . . . . . . . . . . . 12 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → ∀𝑖𝐼𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
2751, 2, 239mat1bas 20993 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ (Base‘(𝐼 Mat 𝑅)))
27613, 14frlmfibas 20841 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ Ring ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
27712, 276sylan2 592 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
2781, 13matbas 20957 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
279278ancoms 459 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
280277, 279eqtrd 2861 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
281275, 280eleqtrrd 2921 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
282 elmapfn 8424 . . . . . . . . . . . . . . . 16 ((1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
283281, 282syl 17 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
284227, 4, 283syl2an 595 . . . . . . . . . . . . . 14 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
285284adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
2861matring 20987 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼 Mat 𝑅) ∈ Ring)
2874, 227, 286syl2anr 596 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝐼 Mat 𝑅) ∈ Ring)
288287adantr 481 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝐼 Mat 𝑅) ∈ Ring)
289 simplr 765 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
290 eqid 2826 . . . . . . . . . . . . . . . . 17 (.r‘(𝐼 Mat 𝑅)) = (.r‘(𝐼 Mat 𝑅))
2912, 290ringcl 19247 . . . . . . . . . . . . . . . 16 (((𝐼 Mat 𝑅) ∈ Ring ∧ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
292288, 221, 289, 291syl3anc 1365 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
293215adantr 481 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
294292, 293eleqtrrd 2921 . . . . . . . . . . . . . 14 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
295 elmapfn 8424 . . . . . . . . . . . . . 14 ((uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
296294, 295syl 17 . . . . . . . . . . . . 13 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
297 eqfnov2 7275 . . . . . . . . . . . . 13 (((1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖𝐼𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
298285, 296, 297syl2anc 584 . . . . . . . . . . . 12 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖𝐼𝑗𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
299274, 298sylibrd 260 . . . . . . . . . . 11 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)))
300299imp 407 . . . . . . . . . 10 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
301300eqcomd 2832 . . . . . . . . 9 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
302 oveq1 7157 . . . . . . . . . . 11 (𝑛 = uncurry 𝑓 → (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
303302eqeq1d 2828 . . . . . . . . . 10 (𝑛 = uncurry 𝑓 → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) ↔ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
304303rspcev 3627 . . . . . . . . 9 ((uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
305222, 301, 304syl2anc 584 . . . . . . . 8 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
306305expl 458 . . . . . . 7 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
307209, 306sylani 603 . . . . . 6 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
308307exlimdv 1927 . . . . 5 ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
309308imp 407 . . . 4 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
310309adantlr 711 . . 3 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗𝐼 ↦ (𝑅 Σg (𝑘𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
311208, 310syldan 591 . 2 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
3126simprbi 497 . . . 4 (𝑅 ∈ Field → 𝑅 ∈ CRing)
313 eqid 2826 . . . . . . . . . 10 (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
314313, 1, 2, 14mdetcl 21140 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
315313, 1, 2, 14mdetcl 21140 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅))
316 eqid 2826 . . . . . . . . . 10 (∥r𝑅) = (∥r𝑅)
31714, 316, 121dvdsrmul 19334 . . . . . . . . 9 ((((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅)) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
318314, 315, 317syl2an 595 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
319318anandis 674 . . . . . . 7 ((𝑅 ∈ CRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
320319anassrs 468 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
321320adantrr 713 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
322 fveq2 6669 . . . . . . . . 9 ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))))
3231, 2, 313, 121, 290mdetmul 21167 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
3243233expa 1112 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
325324an32s 648 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)))
326313, 1, 239, 233mdet1 21145 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝐼 ∈ Fin) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r𝑅))
3274, 326sylan2 592 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r𝑅))
328327adantr 481 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r𝑅))
329325, 328eqeq12d 2842 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) ↔ (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r𝑅)))
330322, 329syl5ib 245 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r𝑅)))
331330impr 455 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r𝑅))
332331breq2d 5075 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(1r𝑅)))
333 eqid 2826 . . . . . . . 8 (Unit‘𝑅) = (Unit‘𝑅)
334333, 233, 316crngunit 19348 . . . . . . 7 (𝑅 ∈ CRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(1r𝑅)))
335334ad2antrr 722 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(1r𝑅)))
336332, 335bitr4d 283 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
337321, 336mpbid 233 . . . 4 (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
338312, 337sylanl1 676 . . 3 (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
339338ad4ant14 748 . 2 (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
340311, 339rexlimddv 3296 1 ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wex 1773  wcel 2107  wne 3021  wral 3143  wrex 3144  Vcvv 3500  cdif 3937  c0 4295  ifcif 4470  {csn 4564  cotp 4572   class class class wbr 5063  cmpt 5143   × cxp 5552  dom cdm 5554  ran crn 5555  cima 5557   Fn wfn 6349  wf 6350  1-1wf1 6351  1-1-ontowf1o 6353  cfv 6354  (class class class)co 7150  f cof 7401  curry ccur 7927  uncurry cunc 7928  m cmap 8401  cen 8500  Fincfn 8503   finSupp cfsupp 8827  Basecbs 16478  .rcmulr 16561  Scalarcsca 16563   ·𝑠 cvsca 16564  0gc0g 16708   Σg cgsu 16709  1rcur 19187  Ringcrg 19233  CRingccrg 19234  rcdsr 19324  Unitcui 19325  DivRingcdr 19438  Fieldcfield 19439  LModclmod 19570  LSpanclspn 19679  LBasisclbs 19782  NzRingcnzr 19965   freeLMod cfrlm 20825   unitVec cuvc 20861   LIndF clindf 20883  LIndSclinds 20884   maMul cmmul 20929   Mat cmat 20951   maDet cmdat 21128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-xor 1498  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-ot 4573  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7574  df-1st 7685  df-2nd 7686  df-supp 7827  df-tpos 7888  df-cur 7929  df-unc 7930  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8284  df-map 8403  df-pm 8404  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-sup 8900  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-xnn0 11962  df-z 11976  df-dec 12093  df-uz 12238  df-rp 12385  df-fz 12888  df-fzo 13029  df-seq 13365  df-exp 13425  df-hash 13686  df-word 13857  df-lsw 13910  df-concat 13918  df-s1 13945  df-substr 13998  df-pfx 14028  df-splice 14107  df-reverse 14116  df-s2 14205  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-0g 16710  df-gsum 16711  df-prds 16716  df-pws 16718  df-mre 16852  df-mrc 16853  df-mri 16854  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18051  df-minusg 18052  df-sbg 18053  df-mulg 18170  df-subg 18221  df-ghm 18301  df-gim 18344  df-cntz 18392  df-oppg 18419  df-symg 18441  df-pmtr 18506  df-psgn 18555  df-evpm 18556  df-cmn 18844  df-abl 18845  df-mgp 19176  df-ur 19188  df-srg 19192  df-ring 19235  df-cring 19236  df-oppr 19309  df-dvdsr 19327  df-unit 19328  df-invr 19358  df-dvr 19369  df-rnghom 19403  df-drng 19440  df-field 19441  df-subrg 19469  df-lmod 19572  df-lss 19640  df-lsp 19680  df-lmhm 19730  df-lbs 19783  df-lvec 19811  df-sra 19880  df-rgmod 19881  df-nzr 19966  df-cnfld 20481  df-zring 20553  df-zrh 20586  df-dsmm 20811  df-frlm 20826  df-uvc 20862  df-lindf 20885  df-linds 20886  df-mamu 20930  df-mat 20952  df-mdet 21129
This theorem is referenced by:  matunitlindf  34776
  Copyright terms: Public domain W3C validator