Theorem matunitlindflem2 33406

Description: One direction of matunitlindf 33407. (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.

Step	Hyp	Ref	Expression
1		eqid 2622	. . . . . . 7 ⊢ (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
2		eqid 2622	. . . . . . 7 ⊢ (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
3	1, 2	matrcl 20218	. . . . . 6 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V))
4	3	simpld 475	. . . . 5 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin)
5	4	ad3antlr 767	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
6		isfld 18756	. . . . . . 7 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
7	6	simplbi 476	. . . . . 6 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
8	7	anim1i 592	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
9	4	ad2antrl 764	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin)
10		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
11		xpfi 8231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
12	11	anidms 677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
13		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
14		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑅) = (Base‘𝑅)
15	13, 14	frlmfibas 20105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
16	12, 15	sylan2 491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
17	1, 13	matbas 20219	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
18	17	ancoms 469	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
19	16, 18	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
20	19	eleq2d 2687	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
21	4, 20	sylan2 491	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
22		fvex 6201	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝑅) ∈ V
23	4, 4, 11	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 × 𝐼) ∈ Fin)
24		elmapg 7870	. . . . . . . . . . . . . . . . . 18 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
25	22, 23, 24	sylancr 695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
26	25	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
27	21, 26	bitr3d 270	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
28	10, 27	mpbid 222	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
29	28	adantrr 753	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
30		eldifsn 4317	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
31	30	biimpri 218	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
32	4, 31	sylan 488	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
33	32	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ (Fin ∖ {∅}))
34		curf 33387	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅}) ∧ (Base‘𝑅) ∈ V) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
35	22, 34	mp3an3 1413	. . . . . . . . . . . . 13 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅})) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
36	29, 33, 35	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
37	9, 36	jca 554	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)))
38	37	ex 450	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
39	38	imdistani 726	. . . . . . . . 9 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
40	39	anassrs 680	. . . . . . . 8 ⊢ (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
41		anass 681	. . . . . . . 8 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ↔ (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))))
42	40, 41	sylibr 224	. . . . . . 7 ⊢ (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)))
43		drngring 18754	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
44		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼)
45		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
46		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝑅 freeLMod 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))
47	44, 45, 46	uvcff 20130	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
48	43, 47	sylan 488	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
49	48	ffvelrnda 6359	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
50	49	ad4ant14 1293	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
51		ffn 6045	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → curry 𝑀 Fn 𝐼)
52		fnima 6010	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀 Fn 𝐼 → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
53	51, 52	syl 17	. . . . . . . . . . . . . . 15 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
54	53	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
55	54	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
56	55	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
57		simplll 798	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝑅 ∈ DivRing)
58		simpllr 799	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
59	45	frlmlmod 20093	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
60	43, 59	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
61	60	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
62		lindfrn 20160	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
63	61, 62	sylan 488	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
64	45	frlmsca 20097	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
65		drngnzr 19262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
66	65	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing)
67	64, 66	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)
68	60, 67	jca 554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing))
69		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Scalar‘(𝑅 freeLMod 𝐼)) = (Scalar‘(𝑅 freeLMod 𝐼))
70	46, 69	lindff1 20159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
71	70	3expa 1265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
72	68, 71	sylan 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
73		fdm 6051	. . . . . . . . . . . . . . . . . . 19 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → dom curry 𝑀 = 𝐼)
74		f1eq2 6097	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom curry 𝑀 = 𝐼 → (curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)) ↔ curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼))))
75	74	biimpac 503	. . . . . . . . . . . . . . . . . . 19 ⊢ ((curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)) ∧ dom curry 𝑀 = 𝐼) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
76	72, 73, 75	syl2an 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
77	76	an32s 846	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
78		f1f1orn 6148	. . . . . . . . . . . . . . . . 17 ⊢ (curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1-onto→ran curry 𝑀)
79	77, 78	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1-onto→ran curry 𝑀)
80		f1oeng 7974	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ curry 𝑀:𝐼–1-1-onto→ran curry 𝑀) → 𝐼 ≈ ran curry 𝑀)
81	58, 79, 80	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ≈ ran curry 𝑀)
82	81	ensymd 8007	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ≈ 𝐼)
83		lindsenlbs 33404	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ran curry 𝑀 ≈ 𝐼) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
84	57, 58, 63, 82, 83	syl31anc 1329	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
85		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (LBasis‘(𝑅 freeLMod 𝐼)) = (LBasis‘(𝑅 freeLMod 𝐼))
86		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(𝑅 freeLMod 𝐼)) = (LSpan‘(𝑅 freeLMod 𝐼))
87	46, 85, 86	lbssp 19079	. . . . . . . . . . . . 13 ⊢ (ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
88	84, 87	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
89	56, 88	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
90	89	adantr 481	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
91	50, 90	eleqtrrd 2704	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)))
92		eqid 2622	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))
93		eqid 2622	. . . . . . . . . . . . 13 ⊢ (0g‘(Scalar‘(𝑅 freeLMod 𝐼))) = (0g‘(Scalar‘(𝑅 freeLMod 𝐼)))
94		eqid 2622	. . . . . . . . . . . . 13 ⊢ ( ·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠 ‘(𝑅 freeLMod 𝐼))
95	45, 14	frlmfibas 20105	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
96	95	feq3d 6032	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ↔ curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼))))
97	96	biimpa 501	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
98	59	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
99		simplr 792	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → 𝐼 ∈ Fin)
100	86, 46, 92, 69, 93, 94, 97, 98, 99	elfilspd 20142	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
101	45	frlmsca 20097	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
102	101	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘𝑅) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))))
103	102	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼))
104	103	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → ((Base‘𝑅) ↑𝑚 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼))
105		elmapi 7879	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼) → 𝑛:𝐼⟶(Base‘𝑅))
106		ffn 6045	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛:𝐼⟶(Base‘𝑅) → 𝑛 Fn 𝐼)
107	106	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑛 Fn 𝐼)
108	51	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀 Fn 𝐼)
109		simpllr 799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝐼 ∈ Fin)
110		inidm 3822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∩ 𝐼) = 𝐼
111		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) = (𝑛‘𝑘))
112		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) = (curry 𝑀‘𝑘))
113	107, 108, 109, 109, 110, 111, 112	offval 6904	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))))
114		simp-4r 807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝐼 ∈ Fin)
115		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛:𝐼⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
116	115	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
117		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼))
118	117	ad4ant24 1298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼))
119	95	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((Base‘𝑅) ↑𝑚 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
120	118, 119	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ (Base‘(𝑅 freeLMod 𝐼)))
121		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (.r‘𝑅) = (.r‘𝑅)
122	45, 46, 14, 114, 116, 120, 94, 121	frlmvscafval 20109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = ((𝐼 × {(𝑛‘𝑘)}) ∘𝑓 (.r‘𝑅)(curry 𝑀‘𝑘)))
123		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛‘𝑘) ∈ V
124		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛‘𝑘) ∈ V → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
125	123, 124	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
126		elmapfn 7880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
127	117, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
128	127	ad4ant24 1298	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
129	123	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
130	129	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
131		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = ((curry 𝑀‘𝑘)‘𝑗))
132	125, 128, 114, 114, 110, 130, 131	offval 6904	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)}) ∘𝑓 (.r‘𝑅)(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
133	122, 132	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
134	133	mpteq2dva 4744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
135	113, 134	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
136	135	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)) = ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
137		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(𝑅 freeLMod 𝐼)) = (0g‘(𝑅 freeLMod 𝐼))
138		simplll 798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑅 ∈ Ring)
139		simp-5l 808	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Ring)
140	115	ad4ant23 1297	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
141		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼))
142		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑𝑚 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
143	117, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
144	143	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
145	141, 144	sylanl1 682	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
146	14, 121	ringcl 18561	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ (𝑛‘𝑘) ∈ (Base‘𝑅) ∧ ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅)) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
147	139, 140, 145, 146	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
148		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))
149	147, 148	fmptd 6385	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅))
150		elmapg 7870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Base‘𝑅) ∈ V ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
151	22, 150	mpan 706	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
152	151	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
153	95	eleq2d 2687	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑𝑚 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
154	152, 153	bitr3d 270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
155	154	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
156	149, 155	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼)))
157		mptexg 6484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
158	157	ralrimivw 2967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → ∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
159		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
160	159	fnmpt 6020	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) Fn 𝐼)
161	158, 160	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) Fn 𝐼)
162		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → 𝐼 ∈ Fin)
163		fvexd 6203	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (0g‘(𝑅 freeLMod 𝐼)) ∈ V)
164	161, 162, 163	fndmfifsupp 8288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
165	164	ad3antlr 767	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
166	45, 46, 137, 109, 109, 138, 156, 165	frlmgsum 20111	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
167	136, 166	eqtr2d 2657	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
168	105, 167	sylan2 491	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
169	168	eqeq2d 2632	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
170	104, 169	rexeqbidva 3155	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘𝑓 ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
171	100, 170	bitr4d 271	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
172	43, 171	sylanl1 682	. . . . . . . . . 10 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
173	172	ad2antrr 762	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
174	91, 173	mpbid 222	. . . . . . . 8 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
175	174	ralrimiva 2966	. . . . . . 7 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
176	42, 175	sylan 488	. . . . . 6 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
177	10, 21	mpbird 247	. . . . . . . . 9 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
178		elmapfn 7880	. . . . . . . . 9 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) → 𝑀 Fn (𝐼 × 𝐼))
179	177, 178	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 Fn (𝐼 × 𝐼))
180	4	adantl 482	. . . . . . . 8 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝐼 ∈ Fin)
181		an32 839	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
182		df-3an 1039	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
183	181, 182	bitr4i 267	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ (𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼))
184		curfv 33389	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
185	183, 184	sylanb 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
186	185	an32s 846	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
187	186	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) = ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
188	187	mpteq2dva 4744	. . . . . . . . . . . . . 14 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
189	188	an32s 846	. . . . . . . . . . . . 13 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
190	189	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
191	190	mpteq2dva 4744	. . . . . . . . . . 11 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
192	191	eqeq2d 2632	. . . . . . . . . 10 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
193	192	rexbidv 3052	. . . . . . . . 9 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
194	193	ralbidv 2986	. . . . . . . 8 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
195	179, 180, 194	syl2anc 693	. . . . . . 7 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
196	195	ad2antrr 762	. . . . . 6 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
197	176, 196	mpbid 222	. . . . 5 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
198	8, 197	sylanl1 682	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
199		fveq1 6190	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = ((𝑓‘𝑖)‘𝑘))
200		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑖 ∈ V
201		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
202		uncov 33390	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ V ∧ 𝑘 ∈ V) → (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘))
203	200, 201, 202	mp2an 708	. . . . . . . . . . 11 ⊢ (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘)
204	199, 203	syl6eqr 2674	. . . . . . . . . 10 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = (𝑖uncurry 𝑓𝑘))
205	204	oveq1d 6665	. . . . . . . . 9 ⊢ (𝑛 = (𝑓‘𝑖) → ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)) = ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
206	205	mpteq2dv 4745	. . . . . . . 8 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
207	206	oveq2d 6666	. . . . . . 7 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
208	207	mpteq2dv 4745	. . . . . 6 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
209	208	eqeq2d 2632	. . . . 5 ⊢ (𝑛 = (𝑓‘𝑖) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
210	209	ac6sfi 8204	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑𝑚 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
211	5, 198, 210	syl2anc 693	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
212		uncf 33388	. . . . . . 7 ⊢ (𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) → uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅))
213	13, 14	frlmfibas 20105	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
214	12, 213	sylan2 491	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
215	1, 13	matbas 20219	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
216	215	ancoms 469	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
217	214, 216	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
218	4, 217	sylan2 491	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
219	218	eleq2d 2687	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅))))
220		elmapg 7870	. . . . . . . . . . . . . 14 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
221	22, 23, 220	sylancr 695	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
222	221	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
223	219, 222	bitr3d 270	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
224	223	biimpar 502	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
225	224	adantr 481	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
226		nfv 1843	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼)
227		nfmpt1 4747	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
228	227	nfeq2 2780	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
229		fveq1 6190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
230	7, 43	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Field → 𝑅 ∈ Ring)
231	230, 4	anim12i 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
232	231	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
233		equcom 1945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 ↔ 𝑗 = 𝑖)
234		ifbi 4107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 = 𝑗 ↔ 𝑗 = 𝑖) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
235	233, 234	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))
236		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘𝑅) = (1r‘𝑅)
237		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0g‘𝑅) = (0g‘𝑅)
238		simpllr 799	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ Fin)
239		simplll 798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Ring)
240		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑖 ∈ 𝐼)
241		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
242		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘(𝐼 Mat 𝑅)) = (1r‘(𝐼 Mat 𝑅))
243	1, 236, 237, 238, 239, 240, 241, 242	mat1ov 20254	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))
244		df-3an 1039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ↔ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼))
245	44, 236, 237	uvcvval 20125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
246	244, 245	sylanbr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
247	235, 243, 246	3eqtr4a 2682	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
248	232, 247	sylanl1 682	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
249		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V
250		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
251	250	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ 𝐼 ∧ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
252	249, 251	mpan2 707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ 𝐼 → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
253	252	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
254		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)
255		simp-4l 806	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Field)
256	4	ad4antlr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ Fin)
257	221	biimpar 502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
258	257	ad5ant23 1304	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
259		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
260	259, 218	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
261	260	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
262		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑖 ∈ 𝐼)
263		simpr 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
264	254, 14, 121, 255, 256, 256, 256, 258, 261, 262, 263	mamufv 20193	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
265	1, 254	matmulr 20244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
266	265	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
267	266	oveqd 6667	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
268	267	oveqd 6667	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
269	4, 268	sylan2 491	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
270	269	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
271	253, 264, 270	3eqtr2rd 2663	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
272	248, 271	eqeq12d 2637	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) ↔ (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗)))
273	229, 272	syl5ibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
274	273	ex 450	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
275	274	com23 86	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑗 ∈ 𝐼 → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
276	226, 228, 275	ralrimd 2959	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
277	276	ralimdva 2962	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
278	1, 2, 242	mat1bas 20255	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ (Base‘(𝐼 Mat 𝑅)))
279	13, 14	frlmfibas 20105	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
280	12, 279	sylan2 491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
281	1, 13	matbas 20219	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
282	281	ancoms 469	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
283	280, 282	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
284	278, 283	eleqtrrd 2704	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
285		elmapfn 7880	. . . . . . . . . . . . . . . 16 ⊢ ((1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
286	284, 285	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
287	230, 4, 286	syl2an 494	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
288	287	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
289	1	matring 20249	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼 Mat 𝑅) ∈ Ring)
290	4, 230, 289	syl2anr 495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝐼 Mat 𝑅) ∈ Ring)
291	290	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝐼 Mat 𝑅) ∈ Ring)
292		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
293		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘(𝐼 Mat 𝑅)) = (.r‘(𝐼 Mat 𝑅))
294	2, 293	ringcl 18561	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 Mat 𝑅) ∈ Ring ∧ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
295	291, 224, 292, 294	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
296	218	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
297	295, 296	eleqtrrd 2704	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)))
298		elmapfn 7880	. . . . . . . . . . . . . 14 ⊢ ((uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑𝑚 (𝐼 × 𝐼)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
299	297, 298	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
300		eqfnov2 6767	. . . . . . . . . . . . 13 ⊢ (((1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
301	288, 299, 300	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
302	277, 301	sylibrd 249	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)))
303	302	imp 445	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
304	303	eqcomd 2628	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
305		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑛 = uncurry 𝑓 → (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
306	305	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑛 = uncurry 𝑓 → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) ↔ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
307	306	rspcev 3309	. . . . . . . . 9 ⊢ ((uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
308	225, 304, 307	syl2anc 693	. . . . . . . 8 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
309	308	expl 648	. . . . . . 7 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
310	212, 309	sylani 686	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
311	310	exlimdv 1861	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
312	311	imp 445	. . . 4 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
313	312	adantlr 751	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑𝑚 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
314	211, 313	syldan 487	. 2 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
315	6	simprbi 480	. . . 4 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
316		eqid 2622	. . . . . . . . . 10 ⊢ (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
317	316, 1, 2, 14	mdetcl 20402	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
318	316, 1, 2, 14	mdetcl 20402	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅))
319		eqid 2622	. . . . . . . . . 10 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
320	14, 319, 121	dvdsrmul 18648	. . . . . . . . 9 ⊢ ((((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅)) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
321	317, 318, 320	syl2an 494	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
322	321	anandis 873	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
323	322	anassrs 680	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
324	323	adantrr 753	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
325		fveq2 6191	. . . . . . . . 9 ⊢ ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))))
326	1, 2, 316, 121, 293	mdetmul 20429	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
327	326	3expa 1265	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
328	327	an32s 846	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
329	316, 1, 242, 236	mdet1 20407	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ Fin) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
330	4, 329	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
331	330	adantr 481	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
332	328, 331	eqeq12d 2637	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) ↔ (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅)))
333	325, 332	syl5ib 234	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅)))
334	333	impr 649	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅))
335	334	breq2d 4665	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
336		eqid 2622	. . . . . . . 8 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
337	336, 236, 319	crngunit 18662	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
338	337	ad2antrr 762	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
339	335, 338	bitr4d 271	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
340	324, 339	mpbid 222	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
341	315, 340	sylanl1 682	. . 3 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
342	341	ad4ant14 1293	. 2 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
343	314, 342	rexlimddv 3035	1 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∖ cdif 3571  ∅c0 3915  ifcif 4086  {csn 4177  ⟨cotp 4185   class class class wbr 4653   ↦ cmpt 4729   × cxp 5112  dom cdm 5114  ran crn 5115   “ cima 5117   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ∘_𝑓 cof 6895  curry ccur 7391  uncurry cunc 7392   ↑_𝑚 cmap 7857   ≈ cen 7952  Fincfn 7955   finSupp cfsupp 8275  Basecbs 15857  ._rcmulr 15942  Scalarcsca 15944   ·_𝑠 cvsca 15945  0_gc0g 16100   Σ_g cgsu 16101  1_rcur 18501  Ringcrg 18547  CRingccrg 18548  ∥_rcdsr 18638  Unitcui 18639  DivRingcdr 18747  Fieldcfield 18748  LModclmod 18863  LSpanclspn 18971  LBasisclbs 19074  NzRingcnzr 19257   freeLMod cfrlm 20090   unitVec cuvc 20121   LIndF clindf 20143  LIndSclinds 20144   maMul cmmul 20189   Mat cmat 20213   maDet cmdat 20390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-xor 1465  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-ot 4186  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-tpos 7352  df-cur 7393  df-unc 7394  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-word 13299  df-lsw 13300  df-concat 13301  df-s1 13302  df-substr 13303  df-splice 13304  df-reverse 13305  df-s2 13593  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-mri 16248  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-gim 17701  df-cntz 17750  df-oppg 17776  df-symg 17798  df-pmtr 17862  df-psgn 17911  df-evpm 17912  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-srg 18506  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-rnghom 18715  df-drng 18749  df-field 18750  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-lmhm 19022  df-lbs 19075  df-lvec 19103  df-sra 19172  df-rgmod 19173  df-nzr 19258  df-cnfld 19747  df-zring 19819  df-zrh 19852  df-dsmm 20076  df-frlm 20091  df-uvc 20122  df-lindf 20145  df-linds 20146  df-mamu 20190  df-mat 20214  df-mdet 20391

This theorem is referenced by:  matunitlindf  33407