isvclem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > isvclem		Structured version Visualization version GIF version

Theorem isvclem 30929

Description: Lemma for isvcOLD 30931. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)

**Hypothesis**
Ref	Expression
isvclem.1	⊢ 𝑋 = ran 𝐺

**Assertion**
Ref	Expression
isvclem	⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (⟨𝐺, 𝑆⟩ ∈ CVec_OLD ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))))

Distinct variable groups: 𝑥,𝑦,𝑧,𝐺 𝑥,𝑆,𝑦,𝑧 𝑥,𝑋,𝑧 Allowed substitution hint: 𝑋(𝑦)

Proof of Theorem isvclem Dummy variables 𝑔 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-vc 30911	. . 3 ⊢ CVec_OLD = {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
2	1	eleq2i 2855	. 2 ⊢ (⟨𝐺, 𝑆⟩ ∈ CVec_OLD ↔ ⟨𝐺, 𝑆⟩ ∈ {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))})
3		eleq1 2851	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑔 ∈ AbelOp ↔ 𝐺 ∈ AbelOp))
4		rneq 5926	. . . . . 6 ⊢ (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
5		isvclem.1	. . . . . 6 ⊢ 𝑋 = ran 𝐺
6	4, 5	eqtr4di 2816	. . . . 5 ⊢ (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
7		xpeq2 5682	. . . . . . 7 ⊢ (ran 𝑔 = 𝑋 → (ℂ × ran 𝑔) = (ℂ × 𝑋))
8	7	feq2d 6689	. . . . . 6 ⊢ (ran 𝑔 = 𝑋 → (𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ↔ 𝑠:(ℂ × 𝑋)⟶ran 𝑔))
9		feq3 6685	. . . . . 6 ⊢ (ran 𝑔 = 𝑋 → (𝑠:(ℂ × 𝑋)⟶ran 𝑔 ↔ 𝑠:(ℂ × 𝑋)⟶𝑋))
10	8, 9	bitrd 282	. . . . 5 ⊢ (ran 𝑔 = 𝑋 → (𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ↔ 𝑠:(ℂ × 𝑋)⟶𝑋))
11	6, 10	syl 18	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ↔ 𝑠:(ℂ × 𝑋)⟶𝑋))
12		oveq 7416	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝑥𝑔𝑧) = (𝑥𝐺𝑧))
13	12	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑦𝑠(𝑥𝑔𝑧)) = (𝑦𝑠(𝑥𝐺𝑧)))
14		oveq 7416	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)))
15	13, 14	eqeq12d 2779	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ↔ (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧))))
16	6, 15	raleqbidv 3338	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ↔ ∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧))))
17		oveq 7416	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)))
18	17	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ↔ ((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥))))
19	18	anbi1d 642	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))) ↔ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))
20	19	ralbidv 3188	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))) ↔ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))
21	16, 20	anbi12d 643	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ((∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))) ↔ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))
22	21	ralbidv 3188	. . . . . 6 ⊢ (𝑔 = 𝐺 → (∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))) ↔ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))
23	22	anbi2d 641	. . . . 5 ⊢ (𝑔 = 𝐺 → (((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))) ↔ ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))))
24	6, 23	raleqbidv 3338	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))) ↔ ∀𝑥 ∈ 𝑋 ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))))
25	3, 11, 24	3anbi123d 1464	. . 3 ⊢ (𝑔 = 𝐺 → ((𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))) ↔ (𝐺 ∈ AbelOp ∧ 𝑠:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))))
26		feq1 6683	. . . 4 ⊢ (𝑠 = 𝑆 → (𝑠:(ℂ × 𝑋)⟶𝑋 ↔ 𝑆:(ℂ × 𝑋)⟶𝑋))
27		oveq 7416	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (1𝑠𝑥) = (1𝑆𝑥))
28	27	eqeq1d 2765	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((1𝑠𝑥) = 𝑥 ↔ (1𝑆𝑥) = 𝑥))
29		oveq 7416	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (𝑦𝑠(𝑥𝐺𝑧)) = (𝑦𝑆(𝑥𝐺𝑧)))
30		oveq 7416	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (𝑦𝑠𝑥) = (𝑦𝑆𝑥))
31		oveq 7416	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (𝑦𝑠𝑧) = (𝑦𝑆𝑧))
32	30, 31	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)))
33	29, 32	eqeq12d 2779	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → ((𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ↔ (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧))))
34	33	ralbidv 3188	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ↔ ∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧))))
35		oveq 7416	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → ((𝑦 + 𝑧)𝑠𝑥) = ((𝑦 + 𝑧)𝑆𝑥))
36		oveq 7416	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (𝑧𝑠𝑥) = (𝑧𝑆𝑥))
37	30, 36	oveq12d 7428	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)))
38	35, 37	eqeq12d 2779	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ↔ ((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥))))
39		oveq 7416	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → ((𝑦 · 𝑧)𝑠𝑥) = ((𝑦 · 𝑧)𝑆𝑥))
40		oveq 7416	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (𝑦𝑠(𝑧𝑠𝑥)) = (𝑦𝑆(𝑧𝑠𝑥)))
41	36	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (𝑦𝑆(𝑧𝑠𝑥)) = (𝑦𝑆(𝑧𝑆𝑥)))
42	40, 41	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (𝑦𝑠(𝑧𝑠𝑥)) = (𝑦𝑆(𝑧𝑆𝑥)))
43	39, 42	eqeq12d 2779	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)) ↔ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))
44	38, 43	anbi12d 643	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → ((((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))) ↔ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))
45	44	ralbidv 3188	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))) ↔ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))
46	34, 45	anbi12d 643	. . . . . . 7 ⊢ (𝑠 = 𝑆 → ((∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))) ↔ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))
47	46	ralbidv 3188	. . . . . 6 ⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))) ↔ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))
48	28, 47	anbi12d 643	. . . . 5 ⊢ (𝑠 = 𝑆 → (((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))) ↔ ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))))
49	48	ralbidv 3188	. . . 4 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑋 ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))) ↔ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))))
50	26, 49	3anbi23d 1467	. . 3 ⊢ (𝑠 = 𝑆 → ((𝐺 ∈ AbelOp ∧ 𝑠:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑠(𝑥𝐺𝑧)) = ((𝑦𝑠𝑥)𝐺(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝐺(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))) ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))))
51	25, 50	opelopabg 5523	. 2 ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (⟨𝐺, 𝑆⟩ ∈ {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))} ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))))
52	2, 51	bitrid 286	1 ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (⟨𝐺, 𝑆⟩ ∈ CVec_OLD ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ∀wral 3079 Vcvv 3455 ⟨cop 4595 {copab 5173 × cxp 5659 ran crn 5662 ⟶wf 6532 (class class class)co 7410 ℂcc 11093 1c1 11096 + caddc 11098 · cmul 11100 AbelOpcablo 30896 CVec_OLDcvc 30910

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-ext 2735 ax-sep 5257 ax-pr 5404

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-sb 2097 df-clab 2742 df-cleq 2755 df-clel 2838 df-ral 3080 df-rab 3417 df-v 3457 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-opab 5174 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-fv 6544 df-ov 7413 df-vc 30911

This theorem is referenced by: isvcOLD 30931

W3C validator