vcoprne - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem vcoprne 8194

Description: The operations of a complex vector space cannot be identical.

**Assertion**
Ref	Expression
vcoprne	⊢ (⟨G, S⟩ ∈ CVec → G ≠ S)

**Proof of Theorem vcoprne**
Step	Hyp	Ref	Expression
1		ax1ne0 5292	. . . . 5 ⊢ 1 ≠ 0
2		df-ne 1590	. . . . 5 ⊢ (1 ≠ 0 ↔ ¬ 1 = 0)
3	1, 2	mpbi 189	. . . 4 ⊢ ¬ 1 = 0
4		vcoprnelem 8193	. . . . . . . . 9 ⊢ (⟨G, G⟩ ∈ CVec → G:(ℂ × ℂ)–→ℂ)
5		axcnex 5279	. . . . . . . . . . 11 ⊢ ℂ ∈ V
6	5, 5	xpex 3266	. . . . . . . . . 10 ⊢ (ℂ × ℂ) ∈ V
7		fex 3658	. . . . . . . . . 10 ⊢ ((G:(ℂ × ℂ)–→ℂ ⋀ (ℂ × ℂ) ∈ V) → G ∈ V)
8	6, 7	mpan2 698	. . . . . . . . 9 ⊢ (G:(ℂ × ℂ)–→ℂ → G ∈ V)
9	4, 8	syl 10	. . . . . . . 8 ⊢ (⟨G, G⟩ ∈ CVec → G ∈ V)
10		op1stg 4093	. . . . . . . 8 ⊢ (G ∈ V → (1^st ‘⟨G, G⟩) = G)
11	9, 10	syl 10	. . . . . . 7 ⊢ (⟨G, G⟩ ∈ CVec → (1^st ‘⟨G, G⟩) = G)
12	11	opreqd 3983	. . . . . 6 ⊢ (⟨G, G⟩ ∈ CVec → (0(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (0G(Id ‘(1^st ‘⟨G, G⟩))))
13	11	rneqd 3347	. . . . . . . . . . . 12 ⊢ (⟨G, G⟩ ∈ CVec → ran (1^st ‘⟨G, G⟩) = ran G)
14		eqid 1478	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘⟨G, G⟩) = (1^st ‘⟨G, G⟩)
15	14	vcgrp 8173	. . . . . . . . . . . . . 14 ⊢ (⟨G, G⟩ ∈ CVec → (1^st ‘⟨G, G⟩) ∈ Grp)
16	11, 15	eqeltrrd 1552	. . . . . . . . . . . . 13 ⊢ (⟨G, G⟩ ∈ CVec → G ∈ Grp)
17		grprndm 8051	. . . . . . . . . . . . 13 ⊢ (G ∈ Grp → ran G = dom dom G)
18	16, 17	syl 10	. . . . . . . . . . . 12 ⊢ (⟨G, G⟩ ∈ CVec → ran G = dom dom G)
19		fdm 3637	. . . . . . . . . . . . . . 15 ⊢ (G:(ℂ × ℂ)–→ℂ → dom G = (ℂ × ℂ))
20	4, 19	syl 10	. . . . . . . . . . . . . 14 ⊢ (⟨G, G⟩ ∈ CVec → dom G = (ℂ × ℂ))
21	20	dmeqd 3319	. . . . . . . . . . . . 13 ⊢ (⟨G, G⟩ ∈ CVec → dom dom G = dom (ℂ × ℂ))
22		dmxpid 3339	. . . . . . . . . . . . 13 ⊢ dom (ℂ × ℂ) = ℂ
23	21, 22	syl6eq 1526	. . . . . . . . . . . 12 ⊢ (⟨G, G⟩ ∈ CVec → dom dom G = ℂ)
24	13, 18, 23	3eqtrd 1514	. . . . . . . . . . 11 ⊢ (⟨G, G⟩ ∈ CVec → ran (1^st ‘⟨G, G⟩) = ℂ)
25		ax1cn 5281	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
26	24, 25	syl5eleqr 1558	. . . . . . . . . 10 ⊢ (⟨G, G⟩ ∈ CVec → 1 ∈ ran (1^st ‘⟨G, G⟩))
27		eqid 1478	. . . . . . . . . . 11 ⊢ ran (1^st ‘⟨G, G⟩) = ran (1^st ‘⟨G, G⟩)
28		eqid 1478	. . . . . . . . . . 11 ⊢ (Id ‘(1^st ‘⟨G, G⟩)) = (Id ‘(1^st ‘⟨G, G⟩))
29	14, 27, 28	vc0rid 8182	. . . . . . . . . 10 ⊢ ((⟨G, G⟩ ∈ CVec ⋀ 1 ∈ ran (1^st ‘⟨G, G⟩)) → (1(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = 1)
30	26, 29	mpdan 706	. . . . . . . . 9 ⊢ (⟨G, G⟩ ∈ CVec → (1(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = 1)
31		eqid 1478	. . . . . . . . . . 11 ⊢ (2^nd ‘⟨G, G⟩) = (2^nd ‘⟨G, G⟩)
32	14, 31, 27	vcid 8166	. . . . . . . . . 10 ⊢ ((⟨G, G⟩ ∈ CVec ⋀ 1 ∈ ran (1^st ‘⟨G, G⟩)) → (1(2^nd ‘⟨G, G⟩)1) = 1)
33	26, 32	mpdan 706	. . . . . . . . 9 ⊢ (⟨G, G⟩ ∈ CVec → (1(2^nd ‘⟨G, G⟩)1) = 1)
34		op2ndg 4094	. . . . . . . . . . . . 13 ⊢ ((G ∈ V ⋀ G ∈ V) → (2^nd ‘⟨G, G⟩) = G)
35	34	anidms 436	. . . . . . . . . . . 12 ⊢ (G ∈ V → (2^nd ‘⟨G, G⟩) = G)
36	9, 35	syl 10	. . . . . . . . . . 11 ⊢ (⟨G, G⟩ ∈ CVec → (2^nd ‘⟨G, G⟩) = G)
37	36, 11	eqtr4d 1513	. . . . . . . . . 10 ⊢ (⟨G, G⟩ ∈ CVec → (2^nd ‘⟨G, G⟩) = (1^st ‘⟨G, G⟩))
38	37	opreqd 3983	. . . . . . . . 9 ⊢ (⟨G, G⟩ ∈ CVec → (1(2^nd ‘⟨G, G⟩)1) = (1(1^st ‘⟨G, G⟩)1))
39	30, 33, 38	3eqtr2d 1516	. . . . . . . 8 ⊢ (⟨G, G⟩ ∈ CVec → (1(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (1(1^st ‘⟨G, G⟩)1))
40	14, 27, 28	vczcl 8181	. . . . . . . . . 10 ⊢ (⟨G, G⟩ ∈ CVec → (Id ‘(1^st ‘⟨G, G⟩)) ∈ ran (1^st ‘⟨G, G⟩))
41	40, 26, 26	3jca 821	. . . . . . . . 9 ⊢ (⟨G, G⟩ ∈ CVec → ((Id ‘(1^st ‘⟨G, G⟩)) ∈ ran (1^st ‘⟨G, G⟩) ⋀ 1 ∈ ran (1^st ‘⟨G, G⟩) ⋀ 1 ∈ ran (1^st ‘⟨G, G⟩)))
42	14, 27	vclcan 8180	. . . . . . . . 9 ⊢ ((⟨G, G⟩ ∈ CVec ⋀ ((Id ‘(1^st ‘⟨G, G⟩)) ∈ ran (1^st ‘⟨G, G⟩) ⋀ 1 ∈ ran (1^st ‘⟨G, G⟩) ⋀ 1 ∈ ran (1^st ‘⟨G, G⟩))) → ((1(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (1(1^st ‘⟨G, G⟩)1) ↔ (Id ‘(1^st ‘⟨G, G⟩)) = 1))
43	41, 42	mpdan 706	. . . . . . . 8 ⊢ (⟨G, G⟩ ∈ CVec → ((1(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (1(1^st ‘⟨G, G⟩)1) ↔ (Id ‘(1^st ‘⟨G, G⟩)) = 1))
44	39, 43	mpbid 195	. . . . . . 7 ⊢ (⟨G, G⟩ ∈ CVec → (Id ‘(1^st ‘⟨G, G⟩)) = 1)
45	44	opreq2d 3982	. . . . . 6 ⊢ (⟨G, G⟩ ∈ CVec → (0G(Id ‘(1^st ‘⟨G, G⟩))) = (0G1))
46	12, 45	eqtr2d 1511	. . . . 5 ⊢ (⟨G, G⟩ ∈ CVec → (0G1) = (0(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))))
47		0cn 5340	. . . . . . 7 ⊢ 0 ∈ ℂ
48	14, 31, 27, 28	vcz 8185	. . . . . . 7 ⊢ ((⟨G, G⟩ ∈ CVec ⋀ 0 ∈ ℂ) → (0(2^nd ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (Id ‘(1^st ‘⟨G, G⟩)))
49	47, 48	mpan2 698	. . . . . 6 ⊢ (⟨G, G⟩ ∈ CVec → (0(2^nd ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (Id ‘(1^st ‘⟨G, G⟩)))
50	36	opreqd 3983	. . . . . . 7 ⊢ (⟨G, G⟩ ∈ CVec → (0(2^nd ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (0G(Id ‘(1^st ‘⟨G, G⟩))))
51	50, 45	eqtrd 1510	. . . . . 6 ⊢ (⟨G, G⟩ ∈ CVec → (0(2^nd ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = (0G1))
52	49, 51, 44	3eqtr3d 1518	. . . . 5 ⊢ (⟨G, G⟩ ∈ CVec → (0G1) = 1)
53	24, 47	syl5eleqr 1558	. . . . . 6 ⊢ (⟨G, G⟩ ∈ CVec → 0 ∈ ran (1^st ‘⟨G, G⟩))
54	14, 27, 28	vc0rid 8182	. . . . . 6 ⊢ ((⟨G, G⟩ ∈ CVec ⋀ 0 ∈ ran (1^st ‘⟨G, G⟩)) → (0(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = 0)
55	53, 54	mpdan 706	. . . . 5 ⊢ (⟨G, G⟩ ∈ CVec → (0(1^st ‘⟨G, G⟩)(Id ‘(1^st ‘⟨G, G⟩))) = 0)
56	46, 52, 55	3eqtr3d 1518	. . . 4 ⊢ (⟨G, G⟩ ∈ CVec → 1 = 0)
57	3, 56	mto 106	. . 3 ⊢ ¬ ⟨G, G⟩ ∈ CVec
58		opeq2 2492	. . . 4 ⊢ (G = S → ⟨G, G⟩ = ⟨G, S⟩)
59	58	eleq1d 1543	. . 3 ⊢ (G = S → (⟨G, G⟩ ∈ CVec ↔ ⟨G, S⟩ ∈ CVec))
60	57, 59	mtbii 718	. 2 ⊢ (G = S → ¬ ⟨G, S⟩ ∈ CVec)
61	60	necon2ai 1614	1 ⊢ (⟨G, S⟩ ∈ CVec → G ≠ S)

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 146 ⋀ w3a 777 = wceq 958 ∈ wcel 960 ≠ wne 1588 Vcvv 1814 ⟨cop 2415 × cxp 3174 dom cdm 3176 ran crn 3177 –→wf 3184 ‘cfv 3188 (class class class)co 3969 1^st c1st 4083 2^nd c2nd 4084 ℂcc 5244 0cc0 5246 1c1 5247 Grpcgr 8030 Idcgi 8031 CVeccvc 8160

This theorem is referenced by: vcex 8195 nvex 8226 nvoprne 8302

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2005 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-fo 3202 df-fv 3204 df-rdg 3938 df-opr 3971 df-oprab 3972 df-1st 4085 df-2nd 4086 df-1o 4139 df-oadd 4141 df-omul 4142 df-er 4267 df-ec 4269 df-qs 4272 df-ni 5012 df-pli 5013 df-mi 5014 df-lti 5015 df-plpq 5047 df-mpq 5048 df-enq 5049 df-nq 5050 df-plq 5051 df-mq 5052 df-rq 5053 df-ltq 5054 df-1q 5055 df-np 5098 df-1p 5099 df-plp 5100 df-mp 5101 df-ltp 5102 df-plpr 5176 df-mpr 5177 df-enr 5178 df-nr 5179 df-plr 5180 df-mr 5181 df-ltr 5182 df-0r 5183 df-1r 5184 df-m1r 5185 df-c 5252 df-0 5253 df-1 5254 df-i 5255 df-r 5256 df-plus 5257 df-mul 5258 df-sub 5368 df-neg 5370 df-grp 8034 df-gid 8035 df-ginv 8036 df-abl 8096 df-vc 8161