Theorem matunitlindflem2 38113

Description: One direction of matunitlindf 38114. (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 2762	. . . . . . 7 ⊢ (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
2		eqid 2762	. . . . . . 7 ⊢ (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
3	1, 2	matrcl 22469	. . . . . 6 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V))
4	3	simpld 498	. . . . 5 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin)
5	4	ad3antlr 741	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
6		isfld 20786	. . . . . . 7 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
7	6	simplbi 500	. . . . . 6 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
8	7	anim1i 624	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
9	4	ad2antrl 738	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin)
10		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
11		xpfi 9264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
12	11	anidms 574	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
13		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
14		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑅) = (Base‘𝑅)
15	13, 14	frlmfibas 21811	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
16	12, 15	sylan2 602	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
17	1, 13	matbas 22470	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
18	17	ancoms 462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
19	16, 18	eqtrd 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
20	19	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
21	4, 20	sylan2 602	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
22		fvex 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝑅) ∈ V
23	4, 4, 11	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 × 𝐼) ∈ Fin)
24		elmapg 8820	. . . . . . . . . . . . . . . . . 18 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
25	22, 23, 24	sylancr 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
26	25	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
27	21, 26	bitr3d 283	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
28	10, 27	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
29	28	adantrr 727	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))
30		eldifsn 4746	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
31	30	biimpri 230	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
32	4, 31	sylan 589	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → 𝐼 ∈ (Fin ∖ {∅}))
33	32	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ (Fin ∖ {∅}))
34		curf 38094	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅}) ∧ (Base‘𝑅) ∈ V) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
35	22, 34	mp3an3 1471	. . . . . . . . . . . . 13 ⊢ ((𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ (Fin ∖ {∅})) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
36	29, 33, 35	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
37	9, 36	jca 519	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)))
38	37	ex 416	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅) → (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
39	38	imdistani 576	. . . . . . . . 9 ⊢ ((𝑅 ∈ DivRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ≠ ∅)) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
40	39	anassrs 471	. . . . . . . 8 ⊢ (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
41		anass 472	. . . . . . . 8 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ↔ (𝑅 ∈ DivRing ∧ (𝐼 ∈ Fin ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))))
42	40, 41	sylibr 236	. . . . . . 7 ⊢ (((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)))
43		drngring 20782	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
44		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑅 unitVec 𝐼) = (𝑅 unitVec 𝐼)
45		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
46		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝑅 freeLMod 𝐼)) = (Base‘(𝑅 freeLMod 𝐼))
47	44, 45, 46	uvcff 21840	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
48	43, 47	sylan 589	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 unitVec 𝐼):𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
49	48	ffvelcdmda 7065	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
50	49	ad4ant14 762	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ (Base‘(𝑅 freeLMod 𝐼)))
51		ffn 6691	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → curry 𝑀 Fn 𝐼)
52		fnima 6651	. . . . . . . . . . . . . . . 16 ⊢ (curry 𝑀 Fn 𝐼 → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
53	51, 52	syl 17	. . . . . . . . . . . . . . 15 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
54	53	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (curry 𝑀 “ 𝐼) = ran curry 𝑀)
55	54	fveq2d 6871	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
56	55	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀))
57		simplll 784	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝑅 ∈ DivRing)
58		simpllr 785	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ∈ Fin)
59	45	frlmlmod 21798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
60	43, 59	sylan 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (𝑅 freeLMod 𝐼) ∈ LMod)
61	60	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
62		lindfrn 21870	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
63	61, 62	sylan 589	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼)))
64	45	frlmsca 21802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
65		drngnzr 20794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
66	65	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → 𝑅 ∈ NzRing)
67	64, 66	eqeltrrd 2863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing)
68	60, 67	jca 519	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) → ((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing))
69		eqid 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Scalar‘(𝑅 freeLMod 𝐼)) = (Scalar‘(𝑅 freeLMod 𝐼))
70	46, 69	lindff1 21869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
71	70	3expa 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 freeLMod 𝐼) ∈ LMod ∧ (Scalar‘(𝑅 freeLMod 𝐼)) ∈ NzRing) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
72	68, 71	sylan 589	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)))
73		fdm 6701	. . . . . . . . . . . . . . . . . . 19 ⊢ (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) → dom curry 𝑀 = 𝐼)
74		f1eq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom curry 𝑀 = 𝐼 → (curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)) ↔ curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼))))
75	74	biimpac 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((curry 𝑀:dom curry 𝑀–1-1→(Base‘(𝑅 freeLMod 𝐼)) ∧ dom curry 𝑀 = 𝐼) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
76	72, 73, 75	syl2an 605	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
77	76	an32s 662	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)))
78		f1f1orn 6818	. . . . . . . . . . . . . . . . 17 ⊢ (curry 𝑀:𝐼–1-1→(Base‘(𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1-onto→ran curry 𝑀)
79	77, 78	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → curry 𝑀:𝐼–1-1-onto→ran curry 𝑀)
80		f1oeng 8951	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ curry 𝑀:𝐼–1-1-onto→ran curry 𝑀) → 𝐼 ≈ ran curry 𝑀)
81	58, 79, 80	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → 𝐼 ≈ ran curry 𝑀)
82	81	ensymd 8986	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ≈ 𝐼)
83		lindsenlbs 38111	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ ran curry 𝑀 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ ran curry 𝑀 ≈ 𝐼) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
84	57, 58, 63, 82, 83	syl31anc 1392	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
85		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (LBasis‘(𝑅 freeLMod 𝐼)) = (LBasis‘(𝑅 freeLMod 𝐼))
86		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(𝑅 freeLMod 𝐼)) = (LSpan‘(𝑅 freeLMod 𝐼))
87	46, 85, 86	lbssp 21143	. . . . . . . . . . . . 13 ⊢ (ran curry 𝑀 ∈ (LBasis‘(𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
88	84, 87	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘ran curry 𝑀) = (Base‘(𝑅 freeLMod 𝐼)))
89	56, 88	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
90	89	adantr 484	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) = (Base‘(𝑅 freeLMod 𝐼)))
91	50, 90	eleqtrrd 2865	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)))
92		eqid 2762	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘(𝑅 freeLMod 𝐼))) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼)))
93		eqid 2762	. . . . . . . . . . . . 13 ⊢ (0g‘(Scalar‘(𝑅 freeLMod 𝐼))) = (0g‘(Scalar‘(𝑅 freeLMod 𝐼)))
94		eqid 2762	. . . . . . . . . . . . 13 ⊢ ( ·𝑠 ‘(𝑅 freeLMod 𝐼)) = ( ·𝑠 ‘(𝑅 freeLMod 𝐼))
95	45, 14	frlmfibas 21811	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
96	95	feq3d 6676	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ↔ curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼))))
97	96	biimpa 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → curry 𝑀:𝐼⟶(Base‘(𝑅 freeLMod 𝐼)))
98	59	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (𝑅 freeLMod 𝐼) ∈ LMod)
99		simplr 778	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → 𝐼 ∈ Fin)
100	86, 46, 92, 69, 93, 94, 97, 98, 99	elfilspd 21852	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
101	45	frlmsca 21802	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → 𝑅 = (Scalar‘(𝑅 freeLMod 𝐼)))
102	101	fveq2d 6871	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘𝑅) = (Base‘(Scalar‘(𝑅 freeLMod 𝐼))))
103	102	oveq1d 7411	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼))
104	103	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → ((Base‘𝑅) ↑m 𝐼) = ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼))
105		elmapi 8830	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((Base‘𝑅) ↑m 𝐼) → 𝑛:𝐼⟶(Base‘𝑅))
106		ffn 6691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛:𝐼⟶(Base‘𝑅) → 𝑛 Fn 𝐼)
107	106	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑛 Fn 𝐼)
108	51	ad2antlr 737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀 Fn 𝐼)
109		simpllr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝐼 ∈ Fin)
110		inidm 4178	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∩ 𝐼) = 𝐼
111		eqidd 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) = (𝑛‘𝑘))
112		eqidd 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) = (curry 𝑀‘𝑘))
113	107, 108, 109, 109, 110, 111, 112	offval 7669	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))))
114		simp-4r 793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝐼 ∈ Fin)
115		ffvelcdm 7062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛:𝐼⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
116	115	adantll 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
117		ffvelcdm 7062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
118	117	ad4ant24 764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼))
119	95	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((Base‘𝑅) ↑m 𝐼) = (Base‘(𝑅 freeLMod 𝐼)))
120	118, 119	eleqtrd 2864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) ∈ (Base‘(𝑅 freeLMod 𝐼)))
121		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (.r‘𝑅) = (.r‘𝑅)
122	45, 46, 14, 114, 116, 120, 94, 121	frlmvscafval 21815	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = ((𝐼 × {(𝑛‘𝑘)}) ∘f (.r‘𝑅)(curry 𝑀‘𝑘)))
123		fvex 6880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛‘𝑘) ∈ V
124		fnconstg 6752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛‘𝑘) ∈ V → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
125	123, 124	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐼 × {(𝑛‘𝑘)}) Fn 𝐼)
126		elmapfn 8846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
127	117, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
128	127	ad4ant24 764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘) Fn 𝐼)
129	123	fvconst2 7188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
130	129	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)})‘𝑗) = (𝑛‘𝑘))
131		eqidd 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = ((curry 𝑀‘𝑘)‘𝑗))
132	125, 128, 114, 114, 110, 130, 131	offval 7669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐼 × {(𝑛‘𝑘)}) ∘f (.r‘𝑅)(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
133	122, 132	eqtrd 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘)) = (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
134	133	mpteq2dva 5193	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)( ·𝑠 ‘(𝑅 freeLMod 𝐼))(curry 𝑀‘𝑘))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
135	113, 134	eqtrd 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))
136	135	oveq2d 7412	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)) = ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
137		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(𝑅 freeLMod 𝐼)) = (0g‘(𝑅 freeLMod 𝐼))
138		simplll 784	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → 𝑅 ∈ Ring)
139		simp-5l 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Ring)
140	115	ad4ant23 763	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑛‘𝑘) ∈ (Base‘𝑅))
141		simplr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼))
142		elmapi 8830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((curry 𝑀‘𝑘) ∈ ((Base‘𝑅) ↑m 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
143	117, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) → (curry 𝑀‘𝑘):𝐼⟶(Base‘𝑅))
144	143	ffvelcdmda 7065	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
145	141, 144	sylanl1 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅))
146	14, 121	ringcl 20296	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ (𝑛‘𝑘) ∈ (Base‘𝑅) ∧ ((curry 𝑀‘𝑘)‘𝑗) ∈ (Base‘𝑅)) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
147	139, 140, 145, 146	syl3anc 1390	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) ∈ (Base‘𝑅))
148	147	fmpttd 7096	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅))
149		elmapg 8820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Base‘𝑅) ∈ V ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
150	22, 149	mpan 700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
151	150	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅)))
152	95	eleq2d 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ ((Base‘𝑅) ↑m 𝐼) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
153	151, 152	bitr3d 283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
154	153	ad3antrrr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))):𝐼⟶(Base‘𝑅) ↔ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼))))
155	148, 154	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ (Base‘(𝑅 freeLMod 𝐼)))
156		mptexg 7205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ Fin → (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
157	156	ralrimivw 3158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ Fin → ∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V)
158		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))
159	158	fnmpt 6661	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑘 ∈ 𝐼 (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) ∈ V → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) Fn 𝐼)
160	157, 159	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) Fn 𝐼)
161		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → 𝐼 ∈ Fin)
162		fvexd 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ Fin → (0g‘(𝑅 freeLMod 𝐼)) ∈ V)
163	160, 161, 162	fndmfifsupp 9324	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ Fin → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
164	163	ad3antlr 741	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) finSupp (0g‘(𝑅 freeLMod 𝐼)))
165	45, 46, 137, 109, 109, 138, 155, 164	frlmgsum 21821	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → ((𝑅 freeLMod 𝐼) Σg (𝑘 ∈ 𝐼 ↦ (𝑗 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
166	136, 165	eqtr2d 2798	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛:𝐼⟶(Base‘𝑅)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
167	105, 166	sylan2 602	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀)))
168	167	eqeq2d 2773	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ 𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
169	104, 168	rexeqbidva 3327	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘(Scalar‘(𝑅 freeLMod 𝐼))) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = ((𝑅 freeLMod 𝐼) Σg (𝑛 ∘f ( ·𝑠 ‘(𝑅 freeLMod 𝐼))curry 𝑀))))
170	100, 169	bitr4d 284	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
171	43, 170	sylanl1 690	. . . . . . . . . 10 ⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
172	171	ad2antrr 736	. . . . . . . . 9 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) ∈ ((LSpan‘(𝑅 freeLMod 𝐼))‘(curry 𝑀 “ 𝐼)) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))))))
173	91, 172	mpbid 234	. . . . . . . 8 ⊢ (((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ 𝑖 ∈ 𝐼) → ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
174	173	ralrimiva 3154	. . . . . . 7 ⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin) ∧ curry 𝑀:𝐼⟶((Base‘𝑅) ↑m 𝐼)) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
175	42, 174	sylan 589	. . . . . 6 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))))
176	10, 21	mpbird 259	. . . . . . . . 9 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
177		elmapfn 8846	. . . . . . . . 9 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → 𝑀 Fn (𝐼 × 𝐼))
178	176, 177	syl 17	. . . . . . . 8 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 Fn (𝐼 × 𝐼))
179	4	adantl 485	. . . . . . . 8 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝐼 ∈ Fin)
180		an32 656	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
181		df-3an 1100	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ↔ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼))
182	180, 181	bitr4i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ↔ (𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼))
183		curfv 38096	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
184	182, 183	sylanb 590	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝑘 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
185	184	an32s 662	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((curry 𝑀‘𝑘)‘𝑗) = (𝑘𝑀𝑗))
186	185	oveq2d 7412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑘 ∈ 𝐼) → ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)) = ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
187	186	mpteq2dva 5193	. . . . . . . . . . . . . 14 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝑗 ∈ 𝐼) ∧ 𝐼 ∈ Fin) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
188	187	an32s 662	. . . . . . . . . . . . 13 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
189	188	oveq2d 7412	. . . . . . . . . . . 12 ⊢ (((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) ∧ 𝑗 ∈ 𝐼) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
190	189	mpteq2dva 5193	. . . . . . . . . . 11 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
191	190	eqeq2d 2773	. . . . . . . . . 10 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
192	191	rexbidv 3186	. . . . . . . . 9 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
193	192	ralbidv 3185	. . . . . . . 8 ⊢ ((𝑀 Fn (𝐼 × 𝐼) ∧ 𝐼 ∈ Fin) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
194	178, 179, 193	syl2anc 593	. . . . . . 7 ⊢ ((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
195	194	ad2antrr 736	. . . . . 6 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → (∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)((curry 𝑀‘𝑘)‘𝑗))))) ↔ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
196	175, 195	mpbid 234	. . . . 5 ⊢ ((((𝑅 ∈ DivRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
197	8, 196	sylanl1 690	. . . 4 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
198		fveq1 6866	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = ((𝑓‘𝑖)‘𝑘))
199		uncov 38097	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ V ∧ 𝑘 ∈ V) → (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘))
200	199	el2v 3461	. . . . . . . . . . 11 ⊢ (𝑖uncurry 𝑓𝑘) = ((𝑓‘𝑖)‘𝑘)
201	198, 200	eqtr4di 2815	. . . . . . . . . 10 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑛‘𝑘) = (𝑖uncurry 𝑓𝑘))
202	201	oveq1d 7411	. . . . . . . . 9 ⊢ (𝑛 = (𝑓‘𝑖) → ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)) = ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))
203	202	mpteq2dv 5194	. . . . . . . 8 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))) = (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))
204	203	oveq2d 7412	. . . . . . 7 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
205	204	mpteq2dv 5194	. . . . . 6 ⊢ (𝑛 = (𝑓‘𝑖) → (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))
206	205	eqeq2d 2773	. . . . 5 ⊢ (𝑛 = (𝑓‘𝑖) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) ↔ ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
207	206	ac6sfi 9228	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑖 ∈ 𝐼 ∃𝑛 ∈ ((Base‘𝑅) ↑m 𝐼)((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑛‘𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
208	5, 197, 207	syl2anc 593	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))))
209		uncf 38095	. . . . . . 7 ⊢ (𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) → uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅))
210	13, 14	frlmfibas 21811	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
211	12, 210	sylan2 602	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
212	1, 13	matbas 22470	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
213	212	ancoms 462	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
214	211, 213	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
215	4, 214	sylan2 602	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
216	215	eleq2d 2848	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅))))
217		elmapg 8820	. . . . . . . . . . . . . 14 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
218	22, 23, 217	sylancr 596	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
219	218	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
220	216, 219	bitr3d 283	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)))
221	220	biimpar 481	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
222	221	adantr 484	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)))
223		nfv 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼)
224		nfmpt1 5199	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗(𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
225	224	nfeq2 2941	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
226		fveq1 6866	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
227	7, 43	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ Field → 𝑅 ∈ Ring)
228	227, 4	anim12i 622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
229	228	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝑅 ∈ Ring ∧ 𝐼 ∈ Fin))
230		equcom 2038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 ↔ 𝑗 = 𝑖)
231		ifbi 4503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 = 𝑗 ↔ 𝑗 = 𝑖) → if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅))
233		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘𝑅) = (1r‘𝑅)
234		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0g‘𝑅) = (0g‘𝑅)
235		simpllr 785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ Fin)
236		simplll 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Ring)
237		simplr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑖 ∈ 𝐼)
238		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
239		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1r‘(𝐼 Mat 𝑅)) = (1r‘(𝐼 Mat 𝑅))
240	1, 233, 234, 235, 236, 237, 238, 239	mat1ov 22505	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))
241		df-3an 1100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ↔ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼))
242	44, 233, 234	uvcvval 21835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
243	241, 242	sylanbr 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = if(𝑗 = 𝑖, (1r‘𝑅), (0g‘𝑅)))
244	232, 240, 243	3eqtr4a 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
245	229, 244	sylanl1 690	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗))
246		ovex 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V
247		eqid 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
248	247	fvmpt2 6987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ 𝐼 ∧ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))) ∈ V) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
249	246, 248	mpan2 701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ 𝐼 → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
250	249	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
251		eqid 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)
252		simp-4l 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑅 ∈ Field)
253	4	ad4antlr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ Fin)
254	218	biimpar 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
255	254	ad5ant23 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → uncurry 𝑓 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
256		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
257	256, 215	eleqtrrd 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
258	257	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
259		simplr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑖 ∈ 𝐼)
260		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
261	251, 14, 121, 252, 253, 253, 253, 255, 258, 259, 260	mamufv 22451	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))
262	1, 251	matmulr 22495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
263	262	ancoms 462	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩) = (.r‘(𝐼 Mat 𝑅)))
264	263	oveqd 7413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
265	264	oveqd 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
266	4, 265	sylan2 602	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
267	266	ad3antrrr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(𝑅 maMul ⟨𝐼, 𝐼, 𝐼⟩)𝑀)𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))
268	250, 261, 267	3eqtr2rd 2804	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗))
269	245, 268	eqeq12d 2778	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗) ↔ (((𝑅 unitVec 𝐼)‘𝑖)‘𝑗) = ((𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))‘𝑗)))
270	226, 269	imbitrrid 248	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
271	270	ex 416	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (𝑗 ∈ 𝐼 → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
272	271	com23 86	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (𝑗 ∈ 𝐼 → (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗))))
273	223, 225, 272	ralrimd 3267	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → (((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
274	273	ralimdva 3174	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
275	1, 2, 239	mat1bas 22506	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ (Base‘(𝐼 Mat 𝑅)))
276	13, 14	frlmfibas 21811	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Ring ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
277	12, 276	sylan2 602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
278	1, 13	matbas 22470	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
279	278	ancoms 462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (Base‘(𝑅 freeLMod (𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅)))
280	277, 279	eqtrd 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
281	275, 280	eleqtrrd 2865	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
282		elmapfn 8846	. . . . . . . . . . . . . . . 16 ⊢ ((1r‘(𝐼 Mat 𝑅)) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
283	281, 282	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ Fin) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
284	227, 4, 283	syl2an 605	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
285	284	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼))
286	1	matring 22500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐼 Mat 𝑅) ∈ Ring)
287	4, 227, 286	syl2anr 606	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝐼 Mat 𝑅) ∈ Ring)
288	287	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (𝐼 Mat 𝑅) ∈ Ring)
289		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))
290		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘(𝐼 Mat 𝑅)) = (.r‘(𝐼 Mat 𝑅))
291	2, 290	ringcl 20296	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 Mat 𝑅) ∈ Ring ∧ uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
292	288, 221, 289, 291	syl3anc 1390	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ (Base‘(𝐼 Mat 𝑅)))
293	215	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅)))
294	292, 293	eleqtrrd 2865	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)))
295		elmapfn 8846	. . . . . . . . . . . . . 14 ⊢ ((uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
296	294, 295	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼))
297		eqfnov2 7526	. . . . . . . . . . . . 13 ⊢ (((1r‘(𝐼 Mat 𝑅)) Fn (𝐼 × 𝐼) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) Fn (𝐼 × 𝐼)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
298	285, 296, 297	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → ((1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) ↔ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (𝑖(1r‘(𝐼 Mat 𝑅))𝑗) = (𝑖(uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)𝑗)))
299	274, 298	sylibrd 261	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) → (∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀)))
300	299	imp 410	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (1r‘(𝐼 Mat 𝑅)) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
301	300	eqcomd 2768	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
302		oveq1 7403	. . . . . . . . . . 11 ⊢ (𝑛 = uncurry 𝑓 → (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀))
303	302	eqeq1d 2764	. . . . . . . . . 10 ⊢ (𝑛 = uncurry 𝑓 → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) ↔ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
304	303	rspcev 3581	. . . . . . . . 9 ⊢ ((uncurry 𝑓 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (uncurry 𝑓(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
305	222, 301, 304	syl2anc 593	. . . . . . . 8 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
306	305	expl 461	. . . . . . 7 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((uncurry 𝑓:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
307	209, 306	sylani 613	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
308	307	exlimdv 1953	. . . . 5 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗)))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅))))
309	308	imp 410	. . . 4 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
310	309	adantlr 725	. . 3 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ ∃𝑓(𝑓:𝐼⟶((Base‘𝑅) ↑m 𝐼) ∧ ∀𝑖 ∈ 𝐼 ((𝑅 unitVec 𝐼)‘𝑖) = (𝑗 ∈ 𝐼 ↦ (𝑅 Σg (𝑘 ∈ 𝐼 ↦ ((𝑖uncurry 𝑓𝑘)(.r‘𝑅)(𝑘𝑀𝑗))))))) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
311	208, 310	syldan 600	. 2 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ∃𝑛 ∈ (Base‘(𝐼 Mat 𝑅))(𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))
312	6	simprbi 501	. . . 4 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
313		eqid 2762	. . . . . . . . . 10 ⊢ (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
314	313, 1, 2, 14	mdetcl 22653	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
315	313, 1, 2, 14	mdetcl 22653	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅))
316		eqid 2762	. . . . . . . . . 10 ⊢ (∥r‘𝑅) = (∥r‘𝑅)
317	14, 316, 121	dvdsrmul 20409	. . . . . . . . 9 ⊢ ((((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑛) ∈ (Base‘𝑅)) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
318	314, 315, 317	syl2an 605	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
319	318	anandis 688	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
320	319	anassrs 471	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
321	320	adantrr 727	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
322		fveq2 6867	. . . . . . . . 9 ⊢ ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))))
323	1, 2, 313, 121, 290	mdetmul 22680	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
324	323	3expa 1131	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
325	324	an32s 662	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)))
326	313, 1, 239, 233	mdet1 22658	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ Fin) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
327	4, 326	sylan2 602	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
328	327	adantr 484	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) = (1r‘𝑅))
329	325, 328	eqeq12d 2778	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘(𝑛(.r‘(𝐼 Mat 𝑅))𝑀)) = ((𝐼 maDet 𝑅)‘(1r‘(𝐼 Mat 𝑅))) ↔ (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅)))
330	322, 329	imbitrid 246	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝑛 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)) → (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅)))
331	330	impr 458	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) = (1r‘𝑅))
332	331	breq2d 5112	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
333		eqid 2762	. . . . . . . 8 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
334	333, 233, 316	crngunit 20423	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
335	334	ad2antrr 736	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(1r‘𝑅)))
336	332, 335	bitr4d 284	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → (((𝐼 maDet 𝑅)‘𝑀)(∥r‘𝑅)(((𝐼 maDet 𝑅)‘𝑛)(.r‘𝑅)((𝐼 maDet 𝑅)‘𝑀)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
337	321, 336	mpbid 234	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
338	312, 337	sylanl1 690	. . 3 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
339	338	ad4ant14 762	. 2 ⊢ (((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ∧ (𝑛 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ (𝑛(.r‘(𝐼 Mat 𝑅))𝑀) = (1r‘(𝐼 Mat 𝑅)))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
340	311, 339	rexlimddv 3169	1 ⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   = wceq 1560  ∃wex 1799   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  Vcvv 3454   ∖ cdif 3901  ∅c0 4285  ifcif 4480  {csn 4582  ⟨cotp 4590   class class class wbr 5100   ↦ cmpt 5181   × cxp 5645  dom cdm 5647  ran crn 5648   “ cima 5650   Fn wfn 6516  ⟶wf 6517  –1-1→wf1 6518  –1-1-onto→wf1o 6520  ‘cfv 6521  (class class class)co 7396   ∘_f cof 7658  curry ccur 8245  uncurry cunc 8246   ↑_m cmap 8808   ≈ cen 8924  Fincfn 8927   finSupp cfsupp 9307  Basecbs 17245  ._rcmulr 17287  Scalarcsca 17289   ·_𝑠 cvsca 17290  0_gc0g 17468   Σ_g cgsu 17469  1_rcur 20227  Ringcrg 20279  CRingccrg 20280  ∥_rcdsr 20399  Unitcui 20400  NzRingcnzr 20558  DivRingcdr 20775  Fieldcfield 20776  LModclmod 20924  LSpanclspn 21035  LBasisclbs 21138   freeLMod cfrlm 21795   unitVec cuvc 21831   LIndF clindf 21853  LIndSclinds 21854   maMul cmmul 22447   Mat cmat 22464   maDet cmdat 22641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150  ax-addf 11152  ax-mulf 11153

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-xor 1532  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-ot 4591  df-uni 4866  df-int 4906  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7660  df-om 7847  df-1st 7970  df-2nd 7971  df-supp 8141  df-tpos 8206  df-cur 8247  df-unc 8248  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8678  df-map 8810  df-pm 8811  df-ixp 8880  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9308  df-sup 9388  df-oi 9458  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-div 11845  df-nn 12211  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12482  df-xnn0 12555  df-z 12569  df-dec 12689  df-uz 12840  df-rp 12994  df-fz 13513  df-fzo 13660  df-seq 14015  df-exp 14075  df-hash 14344  df-word 14527  df-lsw 14576  df-concat 14584  df-s1 14610  df-substr 14655  df-pfx 14685  df-splice 14763  df-reverse 14772  df-s2 14861  df-struct 17183  df-sets 17200  df-slot 17218  df-ndx 17230  df-base 17246  df-ress 17267  df-plusg 17299  df-mulr 17300  df-starv 17301  df-sca 17302  df-vsca 17303  df-ip 17304  df-tset 17305  df-ple 17306  df-ds 17308  df-unif 17309  df-hom 17310  df-cco 17311  df-0g 17470  df-gsum 17471  df-prds 17476  df-pws 17478  df-mre 17614  df-mrc 17615  df-mri 17616  df-acs 17617  df-mgm 18674  df-sgrp 18753  df-mnd 18769  df-mhm 18817  df-submnd 18818  df-efmnd 18903  df-grp 18978  df-minusg 18979  df-sbg 18980  df-mulg 19110  df-subg 19165  df-ghm 19254  df-gim 19299  df-cntz 19357  df-oppg 19386  df-symg 19410  df-pmtr 19482  df-psgn 19531  df-evpm 19532  df-cmn 19822  df-abl 19823  df-mgp 20187  df-rng 20199  df-ur 20228  df-srg 20233  df-ring 20281  df-cring 20282  df-oppr 20382  df-dvdsr 20402  df-unit 20403  df-invr 20433  df-dvr 20446  df-rhm 20517  df-nzr 20559  df-subrng 20592  df-subrg 20616  df-drng 20777  df-field 20778  df-lmod 20926  df-lss 20996  df-lsp 21036  df-lmhm 21086  df-lbs 21139  df-lvec 21167  df-sra 21237  df-rgmod 21238  df-cnfld 21422  df-zring 21496  df-zrh 21552  df-dsmm 21781  df-frlm 21796  df-uvc 21832  df-lindf 21855  df-linds 21856  df-mamu 22448  df-mat 22465  df-mdet 22642

This theorem is referenced by:  matunitlindf  38114